(* filename : prelude.sig
Objective: This file contains all types of functions
for general usage. *)
signature PRELUDE =
sig
val charofdigit : int -> string
val stringofnat : int -> string
val stringofint : int -> string
val file : string -> string
exception Error
val say : string -> 'a
val error : string -> 'a
val member : ''a list -> ''a -> bool
end
(* end of file `prelude.sig' *)
(* File name: cosy.sig
Objective: Create signature for the COSY syntax according to the
definition of General COSY Macro Notation.
[JL93] p.459 (Modified)
The grammar of the Macro COSY program is showed as follows:
M1. <mprogram> = "program" <mprogrambody> "endprogram"
M2. <mprogrambody> = <mpath>
| <mprocess>
| <bodyreplicator>
| <collectivisor> <mprogrambody>
| <mprogrambody> <mpath>
| <mprogrambody> <mprocess>
| <mprogrambody> <bodyreplicator>
M2.1. <collectivisor> = "array" <arraybody> "endarray"
M2.1.1 <arraybody> = <simpleardecl>
| <replardecl>
| <arraybody> <simpleardecl>
| <arraybody> <replardecl>
M2.2. <simpleardecl> = <name1> "(" <simpleardeclbody> ")"
M2.2.1 <name1> = <name>
| <name1> <name>
M2.2.2 <simpleardeclbody> = <iexpr>
| <iexpr> ":" <iexpr>
| <simpleardeclbody> "," <iexpr>
| <simpleardeclbody> "," <iexpr> ":" <iexpr>
M2.3. <replardecl> = <range_spec> "[" <replardeclbody> "]"
M2.3.1 <replardeclbody> = <replardecl>
| <subsevents>
| <replardeclbody> <replardecl>
| <replardeclbody> <subsevents>
M2.4. <subsevents> = <name1> "(" <subseventsbody> ")"
| <subsevents> <name1> "(" <subseventsbody> ")"
M2.4.1 <subseventsbody> = <iexpr>
| <subseventsbody> "," <iexpr>
M2.5. <range_spec>
= "#" <indexvariable> ":" <iexpr> "," <iexpr> "," <iexpr>
M2.6. <iexpr> = <integer>
| <rangevariable>
| <indexvariable>
| <iexpr> "+" <iexpr>
| <iexpr> "*" <iexpr>
| <iexpr> "div" <iexpr>
| <iexpr> "**" <iexpr>
| "(" <iexpr> ")"
M2.7. <space> = " " (* ignored *)
M2.8. <indexvariable> = <name>
M2.9. <rangevariable> = <name>
M2.10. <bodyreplicator> = <range_spec> "[" <b_bodyreplicator> "]"
M2.10.1 <b_bodyreplicator> = <mpath>
| <mprocess>
| <bodyreplicator>
| <b_bodyreplicator> <mpath>
| <b_bodyreplicator> <mprocess>
| <b_bodyreplicator> <bodyreplicator>
M3.1. <mpath> = "path" <msequence> "end"
M3.2. <mprocess> = "process" <msequence> "end"
M4. <msequence> = <morelement>
| <msequence> ";" <morelement>
M5. <morelement> = <gelement>
| <morelement> "," <gelement>
M5.1. <gelement> = <mstarelement>
| <sreplicator>
| <distributor>
| <rreplicator> <gelement>
| <mstarelement> <gelementL>
| <sreplicator> <gelementL>
| <distributor> <gelementL>
M5.2. <gelementL> = <lreplicator>
| <lreplicator> <gelementL>
M6. <mstarelement> = <melement> | <melement> "*"
M7. <melement> = <mevent> | "(" <msequence> ")"
M8. <mevent> = <name>
| <name> "(" ")"
| <name> "(" <meventbody> ")"
M8.1 <meventbody> = Empty
| <iexpr>
| <meventbody> ","
| <meventbody> "," <iexpr>
M9. <distributor> = <sep> <dim> <range> "[" <msequence> "]"
| <sep> <dim> "[" <msequence> "]"
| <sep> <range> "[" <msequence> "]"
| <sep> "[" <msequence> "]"
M9.1. <sep> = "," | ";"
M9.2. <dim> = <iexpr>
M9.3. <range> = "#" <iexpr> "," <iexpr> "," <iexpr>
M10. <sreplicator> = <range_spec> "[" <concseq> "]"
| <range_spec> "[" <imbrseq> "]"
M11. <concseq> = <msequence> <sep> "@"
M12. imbrseq = <msequence> <sep> "@" <sep> "@" <sep> <msequence>
| <msequence> <sep> "@" <sep> <msequence> <sep> "@" <sep> <msequence>
| "(" "@" "@" <sep> <msequence> ")"
| "(" "@" "@" <sep> <msequence> ")" "*"
| "(" "@" <msequence> <sep> "@" <sep> <msequence> ")"
| "(" "@" <msequence> <sep> "@" <sep> <msequence> ")" "*"
| "(" <msequence> <sep> "@" "@" ")"
| "(" <msequence> <sep> "@" "@" ")" "*"
| "(" <msequence> <sep> "@" <sep> <msequence> "@" ")"
| "(" <msequence> <sep> "@" <sep> <msequence> "@" ")" "*"
| "(" "@" <msequence> "@" ")"
| "(" "@" <msequence> "@" ")" "*"
| "(" <imbrseq> ")"
| "(" <imbrseq> ")" "*"
| "(" <msequence> <sep> <imbrseq> ")"
| "(" <msequence> <sep> <imbrseq> ")" "*"
| "(" <imbrseq> <sep> <msequence> ")"
| "(" <imbrseq> <sep> <msequence> ")" "*"
| "(" <msequence> <sep> <imbrseq> <sep> <msequence> ")"
| "(" <msequence> <sep> <imbrseq> <sep> <msequence> ")" "*"
| <msequence> <sep> <imbrseq>
| <imbrseq> <sep> <msequence>
M13. <lreplicator> = <range_spec> "[" <sep> "|" <concseq> "]"
| <range_spec> "[" <sep> "|" <imbrseq> "]"
M14. <rreplicator> = <range_spec> "[" <concseq> "|" <sep> "]"
| <range_spec> "[" <imbrseq> "|" <sep> "]"
M15. <integer> = <digit>
| "-" <digit>
| <integer> <digit>
M16: <name> = <letter>
| <name> <letter>
| <name> <digit>
M17: <letter> = "a"|"b"|"c"|"d"|"e"|"f"|"g"|"h"|"i"|"j"|"k"|"l"|"m"
| "n"|"o"|"p"|"q"|"r"|"s"|"t"|"u"|"v"|"v"|"x"|"y"|"z"
| "A"|"B"|"C"|"D"|"E"|"F"|"G"|"H"|"I"|"J"|"K"|"L"|"M"
| "N"|"O"|"P"|"Q"|"R"|"S"|"T"|"U"|"V"|"W"|"X"|"Y"|"Z"
M18: <digit> = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9" *)
(* The following section is creating datatypes of Macro COSY
syntax according to the grammars given above. *)
signature COSY =
sig
datatype mprogram = Program of mprogrambody
and mprogrambody = Programbody1 of mpath
| Programbody2 of mprocess
| Programbody3 of bodyreplicator
| Programbody4 of collectivisor * mprogrambody
| Programbody5 of mpath * mprogrambody
| Programbody6 of mprocess * mprogrambody
| Programbody7 of bodyreplicator * mprogrambody
and collectivisor = Array of arraybody
and arraybody = Arraybody1 of simpleardecl
| Arraybody2 of replardecl
| Arraybody3 of simpleardecl * arraybody
| Arraybody4 of replardecl * arraybody
and simpleardecl = Simpleardecl of name1 * simpleardeclbody
and name1 = Name1 of name
| Morename of name * name1
and simpleardeclbody = Simpleardeclbody1 of iexpr
| Simpleardeclbody2 of iexpr * iexpr
| Simpleardeclbody3 of iexpr * simpleardeclbody
| Simpleardeclbody4 of iexpr * iexpr * simpleardeclbody
and replardecl = Replardecl of range_spec * replardeclbody
and replardeclbody = Replardeclbody1 of replardecl
| Replardeclbody2 of subsevents
| Replardeclbody3 of replardecl * replardeclbody
| Replardeclbody4 of subsevents * replardeclbody
and subsevents = Subsevents1 of name1 * subseventsbody
| Subsevents2 of name1 * subseventsbody * subsevents
and subseventsbody = Subseventsbody1 of iexpr
| Subseventsbody2 of iexpr * subseventsbody
and range_spec
= Range_spec of indexvariable * iexpr * iexpr * iexpr
and iexpr = Iexpr1 of integer
| Iexpr2 of rangevariable
| Iexpr3 of indexvariable
| Plus of iexpr * iexpr
| Mult of iexpr * iexpr
| Div of iexpr * iexpr
| Pow of iexpr * iexpr
| Iexpr4 of iexpr
and indexvariable = Indexvariable of name
and rangevariable = Rangevariable of name
and bodyreplicator
= Bodyreplicator of range_spec * b_bodyreplicator
and b_bodyreplicator = BBodyreplicator1 of mpath
| BBodyreplicator2 of mprocess
| BBodyreplicator3 of bodyreplicator
| BBodyreplicator4 of mpath * b_bodyreplicator
| BBodyreplicator5 of mprocess * b_bodyreplicator
| BBodyreplicator6 of bodyreplicator * b_bodyreplicator
and mpath = Path of msequence
and mprocess = Process of msequence
and msequence = Sequence1 of morelement
| Sequence2 of morelement * msequence
and morelement = Orelement1 of gelement
| Orelement2 of gelement * morelement
and gelement = Gelement1 of mstarelement
| Gelement2 of sreplicator
| Gelement3 of distributor
| Gelement4 of rreplicator * gelement
| Gelement5 of mstarelement * gelementL
| Gelement5_1 of sreplicator * gelementL
| Gelement5_2 of distributor * gelementL
and gelementL = GelementL1 of lreplicator
| GelementL2 of lreplicator * gelementL
and mstarelement = Nostar of melement
| Star of melement
and melement = Element of mevent
| Group of msequence
and mevent = Event1 of name
| Event2 of name
| Event3 of name * meventbody
and meventbody = Empty
| Meventbody1 of iexpr
| Meventbody2 of meventbody
| Meventbody3 of iexpr * meventbody
| Meventbody4 of iexpr
and distributor = Distributor1 of sep * dim * range * msequence
| Distributor2 of sep * dim * msequence
| Distributor3 of sep * range * msequence
| Distributor4 of sep * msequence
and sep = Comma of string
| Simicol of string
and dim = Dim of iexpr
and range = Range of iexpr * iexpr * iexpr
and sreplicator = Sreplicator1 of range_spec * concseq
| Sreplicator2 of range_spec * imbrseq
and concseq = Concseq of msequence * sep
and imbrseq
= Imbrseq1 of msequence * sep * sep * sep * msequence
| Imbrseq2 of msequence * sep * sep *
msequence * sep * sep * msequence
| Imbrseq3 of sep * msequence
| Imbrseq3s of sep * msequence
| Imbrseq4 of msequence * sep * sep * msequence
| Imbrseq4s of msequence * sep * sep * msequence
| Imbrseq5 of msequence * sep
| Imbrseq5s of msequence * sep
| Imbrseq6 of msequence * sep * sep * msequence
| Imbrseq6s of msequence * sep * sep * msequence
| Imbrseq7 of msequence
| Imbrseq7s of msequence
| Imbrseq8 of imbrseq
| Imbrseq8s of imbrseq
(*| Imbrseq9 of msequence * sep * imbrseq
| Imbrseq9s of msequence * sep * imbrseq
| Imbrseq10 of imbrseq * sep * msequence
| Imbrseq10s of imbrseq * sep * msequence
| Imbrseq11 of msequence * sep * imbrseq * sep * msequence
| Imbrseq11s of msequence * sep * imbrseq * sep * msequence
| Imbrseq12 of msequence * sep * imbrseq
| Imbrseq13 of imbrseq * sep * msequence*)
and lreplicator = Lreplicator1 of range_spec * sep * concseq
| Lreplicator2 of range_spec * sep * imbrseq
and rreplicator = Rreplicator1 of range_spec * concseq * sep
| Rreplicator2 of range_spec * imbrseq * sep
and integer = Integer of int
and name = Name of string;
end
(* Note: According to a lot of testing we did, we found that the
constructors of the datatype imbrseq from Imbrseq9 to
Imbrseq13 which are corresponding to the grammar given
as above are redundant. So, we commentted them out in
order to benefit readers to check whether they are really
redundant. We also commentted the corresponding parts of
the programs which deal with these commentted of the
concrete datatype imbrseq. *)
(* end of file `cosy.sig' *)
(* File name: nmp_lex.sig
Objective: Lexical analyze the COSY environment.
Using the idea of Chris Reade [Rea89]pp.201-222 *)
signature LEX =
sig
datatype token = Operation of string
| Symbol of string
| Number of int
val err_lex : int ref
val keyword : string -> bool
val keycheck : string -> token
val digit : string -> bool
val letter : string -> bool
val letdigetc : string -> bool
val layout : string -> bool
val symbolchar : string -> bool
val intofdigit : string -> int
val lexanal : string list -> token list
val getword : string list -> string list -> token list
val getsymbol : string list -> string list -> token list
val getnum : int -> string list -> token list
val getnum_minus : int -> string list -> token list
end
(* end of file `nmp_lex.sig' *)
(* File name: `parser_prelude.sig'
Objective: These are types of parser builders.
Using the idea of Chris Reade [Rea89]pp.201-222*)
signature PARSER_BUILDER =
sig
structure LX: LEX
datatype 'a possible = Ok of 'a
| Fail
val pair : 'a -> 'b -> 'a * 'b
val <|> : ('a -> 'b possible)
* ('a -> 'b possible) -> 'a -> 'b possible
val modify
: ('a -> ('b * 'c) possible)
* ('b -> 'd) -> 'a -> ('d * 'c) possible
val <&> : ('a -> ('b * 'c) possible) * ('c -> ('d * 'e) possible)
-> 'a -> (('b * 'd) * 'e) possible
val emptyseq : 'a -> ('b list * 'a) possible
val consonto : 'a list -> 'a -> 'a list
val optional : ('a -> ('b * 'a) possible)
-> 'a -> ('b list * 'a) possible
val number : LX.token list -> (int * LX.token list) possible
val literal : string -> LX.token list
-> (string * LX.token list) possible
val operation : LX.token list
-> (string * LX.token list) possible
end
(* end of file `parser_prelude.sig' *)
(* File name: 'nmp_parser.sig'
Objective: Define the type of the parser
Using the idea of Chris Reade [Rea89]pp.201-222*)
signature PARSER =
sig
structure CSY: COSY
structure LX : LEX
structure PRSR_BLDR: PARSER_BUILDER
val m_parser : LX.token list
-> (CSY.mprogram * LX.token list) PRSR_BLDR.possible
end
(* end of file `nmp_parser.sig' *)
(* File name: csr_prelude.sig
Objective: This file contains types of functions that are used
frequently in checking Context-Sensitive
Restrictions *)
signature CSR_PRELUDE =
sig
structure CSY: COSY
structure LX: LEX
val unboundlist : {name:string, value:int} list ref
type unbound
val iex1 : CSY.dim -> int
val iex : CSY.iexpr -> int
val power : int * int -> int
val getvalue : string * {name:string, value:int} list -> int
val cr_unbound_list
: string * {name:string, value:int} list ref -> int
val inp : string -> int
val inp1 : LX.token list * string -> int
end
(* end of file `csr_prelude.sig' *)
(* File name: csr.sig
Objective: Defines the types of functions which checks if the
COSY program satisfies the Context-Sensitive
Restrictions given in [JL92]pp.460-461.
Eech restriction has its own program. *)
signature CSR =
sig
structure CSY: COSY
type Arraytable
type bound
type unbound
val err_cnt : int ref
val mktbl
: CSY.mprogram
-> {dim:int, name:string,
value:{lower:int, pos:int, step:int, upper:int} list} list
val crest1 : CSY.mprogram -> bool
val crest2 : CSY.mprogram -> bool
val crest3 : CSY.mprogram -> bool
val irest1 : CSY.mprogram -> bool
val irest2 : CSY.mprogram -> bool
val brrest : CSY.mprogram -> bool
val rrest11 : CSY.mprogram -> bool
val rrest12 : CSY.mprogram -> bool
val rrest13 : CSY.mprogram -> bool
val rrest2 : CSY.mprogram -> bool
val drest1 : CSY.mprogram -> bool
val drest21 : CSY.mprogram -> bool
val drest22 : CSY.mprogram -> bool
val drest3 : CSY.mprogram -> bool
val drest4 : CSY.mprogram -> bool
val drest5152 : CSY.mprogram -> bool
end
(* end of file `csr.sig' *)
(* File name: transform.sig
Objective: Defines the type of function transform which will
check the whole tree and change the distributor
subtrees into concatenator subtrees.*)
signature TRANSFORM =
sig
structure CSY: COSY
val transform : CSY.mprogram -> CSY.mprogram
end
(* end of file `transform.sig' *)
(* File name: pfirst.sig
Objective: Defines the type of function pathfirst which puts
all the paths in front of the process.*)
signature PFIRST =
sig
structure CSY: COSY
val pathfirst : CSY.mprogram -> int ref -> CSY.mprogram
val chg : int ref
end
(* end of file `pfirst.sig' *)
(* File name: expand.sig
Objective: Define the type of function expand. *)
signature EXPAND =
sig
structure CSY: COSY
val expand : CSY.mprogram -> string
end
(* end of file `expand.sig' *)
(* File name: cosyenv.sig
Objective: This file combines the syntactic analyzer, context-
sensitive restriction checker and expander.*)
signature COSYENV =
sig
val display : string -> unit
val parser_csr_expand : string -> string
end
(* end of file `cosyenv.sig' *)
(* filename : prelude.sml
Objective: This file contains all the functions for
general usage. *)
functor Prelude(): PRELUDE =
struct
val codeof0 = ord "0"
val codeof9 = codeof0 + 9
fun charofdigit n = chr(n+codeof0)
fun stringofnat n = if n<10
then charofdigit n
else stringofnat(n div 10)^charofdigit(n mod 10)
fun stringofint n = if n<0
then "~"^stringofnat(~n)
else stringofnat n
(* read data from a file and output as string *)
fun file x = input(open_in x,10000)
(* display the error message *)
exception Error
fun say (msg: string) = (print msg; print "\n"; raise Error)
fun error msg = say msg
(* check whether b is the element of a list *)
fun member (a :: x) b = if a = b then true else member x b
| member [ ] b = false
end
(* end of file 'prelude.sml' *)
(* File name: cosy.sml
Objective: Create datatype of the COSY program according to the
Syntax of General COSY Macro Notation.
[JL93] p.459 (Modified)
The grammar of the Macro COSY program is showed as follows:
M1. <mprogram> = "program" <mprogrambody> "endprogram"
M2. <mprogrambody> = <mpath>
| <mprocess>
| <bodyreplicator>
| <collectivisor> <mprogrambody>
| <mprogrambody> <mpath>
| <mprogrambody> <mprocess>
| <mprogrambody> <bodyreplicator>
M2.1. <collectivisor> = "array" <arraybody> "endarray"
M2.1.1 <arraybody> = <simpleardecl>
| <replardecl>
| <arraybody> <simpleardecl>
| <arraybody> <replardecl>
M2.2. <simpleardecl> = <name1> "(" <simpleardeclbody> ")"
M2.2.1 <name1> = <name>
| <name1> <name>
M2.2.2 <simpleardeclbody> = <iexpr>
| <iexpr> ":" <iexpr>
| <simpleardeclbody> "," <iexpr>
| <simpleardeclbody> "," <iexpr> ":" <iexpr>
M2.3. <replardecl> = <range_spec> "[" <replardeclbody> "]"
M2.3.1 <replardeclbody> = <replardecl>
| <subsevents>
| <replardeclbody> <replardecl>
| <replardeclbody> <subsevents>
M2.4. <subsevents> = <name1> "(" <subseventsbody> ")"
| <subsevents> <name1> "(" <subseventsbody> ")"
M2.4.1 <subseventsbody> = <iexpr>
| <subseventsbody> "," <iexpr>
M2.5. <range_spec>
= "#" <indexvariable> ":" <iexpr> "," <iexpr> "," <iexpr>
M2.6. <iexpr> = <integer>
| <rangevariable>
| <indexvariable>
| <iexpr> "+" <iexpr>
| <iexpr> "*" <iexpr>
| <iexpr> "div" <iexpr>
| <iexpr> "**" <iexpr>
| "(" <iexpr> ")"
M2.7. <space> = " " (* ignored *)
M2.8. <indexvariable> = <name>
M2.9. <rangevariable> = <name>
M2.10. <bodyreplicator> = <range_spec> "[" <b_bodyreplicator> "]"
M2.10.1 <b_bodyreplicator> = <mpath>
| <mprocess>
| <bodyreplicator>
| <b_bodyreplicator> <mpath>
| <b_bodyreplicator> <mprocess>
| <b_bodyreplicator> <bodyreplicator>
M3.1. <mpath> = "path" <msequence> "end"
M3.2. <mprocess> = "process" <msequence> "end"
M4. <msequence> = <morelement>
| <msequence> ";" <morelement>
M5. <morelement> = <gelement>
| <morelement> "," <gelement>
M5.1. <gelement> = <mstarelement>
| <sreplicator>
| <distributor>
| <rreplicator> <gelement>
| <mstarelement> <gelementL>
| <sreplicator> <gelementL>
| <distributor> <gelementL>
M5.2. <gelementL> = <lreplicator>
| <lreplicator> <gelementL>
M6. <mstarelement> = <melement> | <melement> "*"
M7. <melement> = <mevent> | "(" <msequence> ")"
M8. <mevent> = <name>
| <name> "(" ")"
| <name> "(" <meventbody> ")"
M8.1 <meventbody> = Empty
| <iexpr>
| <meventbody> ","
| <meventbody> "," <iexpr>
M9. <distributor> = <sep> <dim> <range> "[" <msequence> "]"
| <sep> <dim> "[" <msequence> "]"
| <sep> <range> "[" <msequence> "]"
| <sep> "[" <msequence> "]"
M9.1. <sep> = "," | ";"
M9.2. <dim> = <iexpr>
M9.3. <range> = "#" <iexpr> "," <iexpr> "," <iexpr>
M10. <sreplicator> = <range_spec> "[" <concseq> "]"
| <range_spec> "[" <imbrseq> "]"
M11. <concseq> = <msequence> <sep> "@"
M12. imbrseq = <msequence> <sep> "@" <sep> "@" <sep> <msequence>
| <msequence> <sep> "@" <sep> <msequence> <sep> "@" <sep> <msequence>
| "(" "@" "@" <sep> <msequence> ")"
| "(" "@" "@" <sep> <msequence> ")" "*"
| "(" "@" <msequence> <sep> "@" <sep> <msequence> ")"
| "(" "@" <msequence> <sep> "@" <sep> <msequence> ")" "*"
| "(" <msequence> <sep> "@" "@" ")"
| "(" <msequence> <sep> "@" "@" ")" "*"
| "(" <msequence> <sep> "@" <sep> <msequence> "@" ")"
| "(" <msequence> <sep> "@" <sep> <msequence> "@" ")" "*"
| "(" "@" <msequence> "@" ")"
| "(" "@" <msequence> "@" ")" "*"
| "(" <imbrseq> ")"
| "(" <imbrseq> ")" "*"
| "(" <msequence> <sep> <imbrseq> ")"
| "(" <msequence> <sep> <imbrseq> ")" "*"
| "(" <imbrseq> <sep> <msequence> ")"
| "(" <imbrseq> <sep> <msequence> ")" "*"
| "(" <msequence> <sep> <imbrseq> <sep> <msequence> ")"
| "(" <msequence> <sep> <imbrseq> <sep> <msequence> ")" "*"
| <msequence> <sep> <imbrseq>
| <imbrseq> <sep> <msequence>
M13. <lreplicator> = <range_spec> "[" <sep> "|" <concseq> "]"
| <range_spec> "[" <sep> "|" <imbrseq> "]"
M14. <rreplicator> = <range_spec> "[" <concseq> "|" <sep> "]"
| <range_spec> "[" <imbrseq> "|" <sep> "]"
M15. <integer> = <digit>
| "-" <digit>
| <integer> <digit>
M16: <name> = <letter>
| <name> <letter>
| <name> <digit>
M17: <letter> = "a"|"b"|"c"|"d"|"e"|"f"|"g"|"h"|"i"|"j"|"k"|"l"|"m"
| "n"|"o"|"p"|"q"|"r"|"s"|"t"|"u"|"v"|"v"|"x"|"y"|"z"
| "A"|"B"|"C"|"D"|"E"|"F"|"G"|"H"|"I"|"J"|"K"|"L"|"M"
| "N"|"O"|"P"|"Q"|"R"|"S"|"T"|"U"|"V"|"W"|"X"|"Y"|"Z"
M18: <digit> = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9" *)
(* The following section is creating datatypes of Macro COSY syntax
according to the grammars given above. *)
functor Cosy(): COSY =
struct
datatype mprogram = Program of mprogrambody
and mprogrambody = Programbody1 of mpath
| Programbody2 of mprocess
| Programbody3 of bodyreplicator
| Programbody4 of collectivisor * mprogrambody
| Programbody5 of mpath * mprogrambody
| Programbody6 of mprocess * mprogrambody
| Programbody7 of bodyreplicator * mprogrambody
and collectivisor = Array of arraybody
and arraybody = Arraybody1 of simpleardecl
| Arraybody2 of replardecl
| Arraybody3 of simpleardecl * arraybody
| Arraybody4 of replardecl * arraybody
and simpleardecl = Simpleardecl of name1 * simpleardeclbody
and name1 = Name1 of name
| Morename of name * name1
and simpleardeclbody = Simpleardeclbody1 of iexpr
| Simpleardeclbody2 of iexpr * iexpr
| Simpleardeclbody3 of iexpr * simpleardeclbody
| Simpleardeclbody4 of iexpr * iexpr * simpleardeclbody
and replardecl = Replardecl of range_spec * replardeclbody
and replardeclbody = Replardeclbody1 of replardecl
| Replardeclbody2 of subsevents
| Replardeclbody3 of replardecl * replardeclbody
| Replardeclbody4 of subsevents * replardeclbody
and subsevents = Subsevents1 of name1 * subseventsbody
| Subsevents2 of name1 * subseventsbody * subsevents
and subseventsbody = Subseventsbody1 of iexpr
| Subseventsbody2 of iexpr * subseventsbody
and range_spec
= Range_spec of indexvariable * iexpr * iexpr * iexpr
and iexpr = Iexpr1 of integer
| Iexpr2 of rangevariable
| Iexpr3 of indexvariable
| Plus of iexpr * iexpr
| Mult of iexpr * iexpr
| Div of iexpr * iexpr
| Pow of iexpr * iexpr
| Iexpr4 of iexpr
and indexvariable = Indexvariable of name
and rangevariable = Rangevariable of name
and bodyreplicator
= Bodyreplicator of range_spec * b_bodyreplicator
and b_bodyreplicator = BBodyreplicator1 of mpath
| BBodyreplicator2 of mprocess
| BBodyreplicator3 of bodyreplicator
| BBodyreplicator4 of mpath * b_bodyreplicator
| BBodyreplicator5 of mprocess * b_bodyreplicator
| BBodyreplicator6 of bodyreplicator * b_bodyreplicator
and mpath = Path of msequence
and mprocess = Process of msequence
and msequence = Sequence1 of morelement
| Sequence2 of morelement * msequence
and morelement = Orelement1 of gelement
| Orelement2 of gelement * morelement
and gelement = Gelement1 of mstarelement
| Gelement2 of sreplicator
| Gelement3 of distributor
| Gelement4 of rreplicator * gelement
| Gelement5 of mstarelement * gelementL
| Gelement5_1 of sreplicator * gelementL
| Gelement5_2 of distributor * gelementL
and gelementL = GelementL1 of lreplicator
| GelementL2 of lreplicator * gelementL
and mstarelement = Nostar of melement
| Star of melement
and melement = Element of mevent
| Group of msequence
and mevent = Event1 of name
| Event2 of name
| Event3 of name * meventbody
and meventbody = Empty
| Meventbody1 of iexpr
| Meventbody2 of meventbody
| Meventbody3 of iexpr * meventbody
| Meventbody4 of iexpr
and distributor = Distributor1 of sep * dim * range * msequence
| Distributor2 of sep * dim * msequence
| Distributor3 of sep * range * msequence
| Distributor4 of sep * msequence
and sep = Comma of string
| Simicol of string
and dim = Dim of iexpr
and range = Range of iexpr * iexpr * iexpr
and sreplicator = Sreplicator1 of range_spec * concseq
| Sreplicator2 of range_spec * imbrseq
and concseq = Concseq of msequence * sep
and imbrseq
= Imbrseq1 of msequence * sep * sep * sep * msequence
| Imbrseq2 of msequence * sep * sep *
msequence * sep * sep * msequence
| Imbrseq3 of sep * msequence
| Imbrseq3s of sep * msequence
| Imbrseq4 of msequence * sep * sep * msequence
| Imbrseq4s of msequence * sep * sep * msequence
| Imbrseq5 of msequence * sep
| Imbrseq5s of msequence * sep
| Imbrseq6 of msequence * sep * sep * msequence
| Imbrseq6s of msequence * sep * sep * msequence
| Imbrseq7 of msequence
| Imbrseq7s of msequence
| Imbrseq8 of imbrseq
| Imbrseq8s of imbrseq
(*| Imbrseq9 of msequence * sep * imbrseq
| Imbrseq9s of msequence * sep * imbrseq
| Imbrseq10 of imbrseq * sep * msequence
| Imbrseq10s of imbrseq * sep * msequence
| Imbrseq11 of msequence * sep * imbrseq * sep * msequence
| Imbrseq11s of msequence * sep * imbrseq * sep * msequence
| Imbrseq12 of msequence * sep * imbrseq
| Imbrseq13 of imbrseq * sep * msequence*)
and lreplicator = Lreplicator1 of range_spec * sep * concseq
| Lreplicator2 of range_spec * sep * imbrseq
and rreplicator = Rreplicator1 of range_spec * concseq * sep
| Rreplicator2 of range_spec * imbrseq * sep
and integer = Integer of int
and name = Name of string;
end
(* Note: According to a lot of testing we did, we found that the
constructors of the datatype imbrseq from Imbrseq9 to
Imbrseq13 which are corresponding to the grammar given
as above are redundant. So, we commentted them out in
order to benefit readers to check whether they are really
redundant. We also commentted the corresponding parts of
the programs which deal with these commentted of the
concrete datatype imbrseq. *)
(* end of file 'nmp_datatype.sml' *)
(* File name: nmp_lex.sml
Objective: Lexical analyze the COSY environment.
Using the idea of Chris Reade [Rea89]pp.201-222
Input : string
Output : token list *)
functor Lex (structure PRLD: PRELUDE): LEX =
struct
val err_lex = ref 0
datatype token = Operation of string
| Symbol of string
| Number of int
val keyword = PRLD.member ["program","endprogram","path",
"process","end","array","endarray"]
fun keycheck s = if keyword s then Symbol s else Operation s
fun digit d = ord d >= ord "0" andalso ord d <= ord "9"
fun letter s
= (ord s >= ord "A" andalso ord s <= ord "Z") orelse
(ord s >= ord "a" andalso ord s <= ord "z")
fun letdigetc a = if letter a then true
else if digit a then true
else PRLD.member ["'","_"] a
val layout = PRLD.member [" ","\n","\t"]
val symbolchar =
PRLD.member ["&","*","[","]",",",";",":","#",
"|","@","div","+","**","-","~"]
fun intofdigit d = ord d - ord "0"
fun lexanal [ ] = [ ]
| lexanal (a::x) = if layout a then lexanal x else
if a = "(" then Symbol "(" :: lexanal x else
if a = ")" then Symbol ")" :: lexanal x else
if a = "-" then getnum_minus 0 x else
if a = "~" then getnum_minus 0 x else
if letter a then getword [a] x else
if digit a then getnum (intofdigit a) x else
if symbolchar a then getsymbol [a] x else
PRLD.error ("Lexical Error : unrecognized token "
^ a) handle PRLD.Error
=> (err_lex := (!err_lex) + 1; lexanal x)
and getword l [ ] = [keycheck (implode (rev l))]
| getword l (a :: x) = if letdigetc a
then getword (a :: l) x
else keycheck (implode (rev l)) :: lexanal (a :: x)
and getsymbol l [ ] = [Symbol (implode (rev l))]
| getsymbol l (a :: x) = if l = ["*"] andalso a = "*"
then Symbol "**" :: lexanal x
else Symbol (implode (rev l)) :: lexanal (a :: x)
and getnum n [ ] = [Number n]
| getnum n (a :: x) = if digit a
then getnum (n * 10 + intofdigit a) x
else Number n :: lexanal (a :: x)
and getnum_minus n [ ] = [Number (0-n)]
| getnum_minus n (a :: x) = if digit a
then getnum_minus (n * 10 + intofdigit a) x
else Number (0-n) :: lexanal (a :: x)
end
(* end of file 'nmp_lex.sml' *)
(* File name: `parser_prelude.sml'
Objective: These are parser builders.
Using the idea of Chris Reade [Rea89]pp.201-222*)
functor Parser_builder(structure LX: LEX): PARSER_BUILDER =
struct
structure LX= LX
datatype 'a possible = Ok of 'a
| Fail
fun pair x y = (x, y)
infixr 4 <&>
infixr 3 <|>
infix 0 modify
fun (parser1 <|> parser2) s
= let fun parser2_if_fail Fail = parser2 s
| parser2_if_fail x = x
in parser2_if_fail (parser1 s) end
fun (parser modify f) s
= let fun modresult Fail = Fail
| modresult (Ok(x, y)) = Ok(f x, y)
in modresult (parser s) end
fun (parser1 <&> parser2) s
= let fun parser2_after Fail = Fail
| parser2_after (Ok(x1, s1))
= (parser2 modify (pair x1)) s1
in parser2_after (parser1 s) end
fun emptyseq s = Ok([], s)
fun consonto x a = a :: x
fun optional pr = (pr modify (consonto []))
<|> emptyseq
fun number (LX.Number n::s) = Ok(n, s)
| number other = Fail
fun literal a (LX.Symbol x::s) = if a = x then Ok(x, s) else Fail
| literal a other = Fail
fun operation (LX.Operation x::s) = Ok(x,s)
| operation other = Fail
end
(* end of file `parser_prelude.sml' *)
(* File name: `nmp_parser.sml'
Objective: Parse the COSY Program
Using the idea of Chris Reade [Rea89]pp.201-222
Input : token list
Output : mprogram (tree) *)
(* THE PARSERS (compare with the grammar [JL92] p.459 (Modified)) *)
functor Parser(structure PRLD: PRELUDE
structure PRSR_BLDR: PARSER_BUILDER
structure CSY: COSY
structure LX: LEX
sharing PRSR_BLDR.LX = LX): PARSER =
struct
structure PRLD = PRLD
structure LX = LX
structure PRSR_BLDR = PRSR_BLDR
structure CSY = CSY
local
open PRLD
open PRSR_BLDR
open CSY
open LX
infixr 4 <&>
infixr 3 <|>
infix 0 modify
fun mprogram1 s = (literal "program" <&> mprogrambody1 <&>
literal "endprogram" modify mp) s
and mprogrambody1 s
= (m_path1 <|> m_process1 <|> m_bodyreplicator1 <|>
m_collectivisor1) s
and m_path1 s
= (mpath1 <&> optional mprogrambody1 modify m_pb1) s
and m_process1 s
= (mprocess1 <&> optional mprogrambody1 modify m_pb2) s
and m_bodyreplicator1 s
= (bodyreplicator1 <&> optional mprogrambody1 modify m_pb3) s
and m_collectivisor1 s
= (collectivisor1 <&> mprogrambody1 modify m_pb4) s
and collectivisor1 s
= (literal "array" <&> arraybody1 <&>
literal "endarray" modify mar) s
and arraybody1 s
= ((simpleardecl1 <&> optional arraybody1 modify ar_1)
<|> (replardecl1 <&> optional arraybody1 modify ar_2)) s
and simpleardecl1 s
= (name11 <&> literal "(" <&> simpleardeclbody1
<&> literal ")" modify simp) s
and name11 s = (name111 <&> optional name11 modify more1) s
and simpleardeclbody1 s =
((iexpr11 <&> literal ":" <&> iexpr11 <&> optional
(literal "," <&> simpleardeclbody1) modify simp_2)
<|> (iexpr11 <&> optional (literal "," <&>
simpleardeclbody1) modify simp_1)) s
and replardecl1 s
= (range_spec1 <&> literal "[" <&> replardeclbody1 <&>
literal "]" modify repl) s
and replardeclbody1 s
= ((replardecl1 <&> optional replardeclbody1 `
modify repl_body1)
<|> (subsevents1 <&> optional replardeclbody1
modify repl_body2)) s
and subsevents1 s
= (name11 <&> literal "(" <&> subseventsbody1 <&>
literal ")" <&> optional subsevents1 modify subs) s
and subseventsbody1 s
= (iexpr11 <&> optional (literal "," <&>
subseventsbody1) modify subs_body) s
and range_spec1 s
= (literal "#" <&> indexvariable1 <&> literal ":" <&>
iexpr11 <&> literal "," <&> iexpr11 <&> literal ","
<&> iexpr11 modify range_s) s
and iexpr11 s = (iexpr1 <&> optional (literal "+" <&> iexpr11)
modify ie_plus) s
and iexpr1 s = (iexpr2 <&> optional (literal "*" <&> iexpr1)
modify ie_mul) s
and iexpr2 s = (iexpr3 <&> optional (literal "div" <&> iexpr2)
modify ie_div) s
and iexpr3 s = (iexpr4 <&> optional (literal "**" <&> iexpr3)
modify ie_pow) s
and iexpr4 s
= ((literal "(" <&> iexpr11 <&> literal ")" modify unparenth)
<|> (integer1 modify int1)
<|> (rangevariable1 modify ran)
<|> (indexvariable1 modify ind)) s
and indexvariable1 s = (name111 modify ind_val) s
and rangevariable1 s = (name111 modify ran_val) s
and bodyreplicator1 s = (range_spec1 <&> literal "[" <&>
b_bodyreplicator1 <&> literal "]"
modify brep) s
and b_bodyreplicator1 s
= ((mpath1 <&> optional b_bodyreplicator1 modify bbrep1)
<|> (mprocess1 <&> optional b_bodyreplicator1
modify bbrep2)
<|> (bodyreplicator1 <&> optional b_bodyreplicator1
modify bbrep3)) s
and mpath1 s = (literal "path" <&> msequence1 <&>
literal "end" modify mpa) s
and mprocess1 s = (literal "process" <&> msequence1 <&>
literal "end" modify mpr) s
and msequence1 s = (morelement1 <&> optional (literal ";" <&>
msequence1) modify mseq) s
and morelement1 s = (gelement1 <&> optional (literal "," <&>
morelement1) modify mor) s
and gelement1 s
= ((mstarelement1 <&> optional gelement2 modify gel2)
<|> (sreplicator1 <&> optional gelement2 modify gel2_1)
<|> (distributor1 <&> optional gelement2 modify gel2_2)
<|> (rreplicator1 <&> gelement1 modify gel_4)) s
and gelement2 s
= (lreplicator1 <&> optional gelement2 modify ge2) s
and mstarelement1 s = (star_element1 <|> nostar_element1) s
and star_element1 s
= (melement1 <&> literal "*" modify mstar) s
and nostar_element1 s = (melement1 modify mnostar) s
and melement1 s = (mevent_only1 <|> mgroup1) s
and mevent_only1 s = (mevent1 modify meo) s
and mgroup1 s
= (literal "(" <&> msequence1 <&> literal ")" modify mgr) s
and mevent1 s
= ((name111 <&> literal "(" <&> literal ")" modify mev2)
<|> (name111 <&> optional (literal "(" <&> meventbody1 <&>
literal ")") modify mev1)) s
and meventbody1 s
= ((iexpr11 <&> optional (literal "," <&>
optional meventbody1) modify mevb2)
<|> (literal "," <&> optional meventbody1
modify mevb1)) s
and distributor1 s
= ((sep1 <&> dim11 <&> range11 <&> literal "[" <&>
msequence1 <&> literal "]" modify dist1)
<|> (sep1 <&> dim11 <&> literal "[" <&>
msequence1 <&> literal "]" modify dist2)
<|> (sep1 <&> range11 <&> literal "[" <&>
msequence1 <&> literal "]" modify dist3)
<|> (sep1 <&> literal "[" <&>
msequence1 <&> literal "]" modify dist4)) s
and sep1 s = ((literal "," modify Comma)
<|> (literal ";" modify Simicol)) s
and dim11 s = (iexpr11 modify dim1) s
and range11 s
= ((literal "#" <&> iexpr11 <&> literal ","<&> iexpr11
<&> literal "," <&> iexpr11 modify range1)) s
and sreplicator1 s = ((range_spec1 <&> literal "[" <&> concseq1
<&> literal "]" modify srep1)
<|> (range_spec1 <&> literal "[" <&> imbrseq1 <&>
literal "]" modify srep2)) s
and concseq1 s
= (msequence1 <&> sep1 <&> literal "@" modify cons) s
and imbrseq1 s
= ((msequence1 <&> sep1 <&> literal "@" <&> sep1 <&>
literal "@" <&> sep1 <&> msequence1 modify imbr1)
<|> (msequence1 <&> sep1 <&> literal "@" <&> sep1 <&>
msequence1 <&> sep1 <&> literal "@" <&> sep1 <&>
msequence1 modify imbr2)
<|> (literal "(" <&> literal "@" <&> literal "@" <&> sep1 <&>
msequence1 <&> literal ")" <&> literal "*" modify imbr3s)
<|> (literal "(" <&> literal "@" <&> literal "@" <&> sep1 <&>
msequence1 <&> literal ")" modify imbr3)
<|> (literal "(" <&> literal "@" <&> msequence1 <&> sep1 <&>
literal "@" <&> sep1 <&> msequence1 <&> literal ")" <&>
literal "*" modify imbr4s)
<|> (literal "(" <&> literal "@" <&> msequence1 <&> sep1 <&>
literal "@" <&> sep1 <&> msequence1 <&> literal ")"
modify imbr4)
<|> (literal "(" <&> msequence1 <&> sep1 <&> literal "@" <&>
literal "@" <&> literal ")" <&> literal "*" modify imbr5s)
<|> (literal "(" <&> msequence1 <&> sep1 <&> literal "@" <&>
literal "@" <&> literal ")" modify imbr5)
<|> (literal "(" <&> msequence1 <&> sep1 <&> literal "@"
<&> sep1 <&> msequence1 <&> literal "@" <&> literal ")"
<&> literal "*" modify imbr6s)
<|> (literal "(" <&> msequence1 <&> sep1 <&> literal "@"
<&> sep1 <&> msequence1 <&> literal "@" <&> literal ")"
modify imbr6)
<|> (literal "(" <&> literal "@" <&> msequence1 <&> literal "@"
<&> literal ")" <&> literal "*" modify imbr7s)
<|> (literal "(" <&> literal "@" <&> msequence1 <&> literal "@"
<&> literal ")" modify imbr7)
<|> (literal "(" <&> imbrseq1 <&> literal ")" <&> literal "*"
modify imbr8s)
<|> (literal "(" <&> imbrseq1 <&> literal ")" modify imbr8)) s
(* <|> (literal "(" <&> msequence <&> sep <&> imbrseq <&>
literal ")" <&> literal "*" modify imbr9s)
<|> (literal "(" <&> msequence <&> sep <&> imbrseq <&>
literal ")" modify imbr9)
<|> (literal "(" <&> imbrseq <&> sep <&> msequence <&>
literal ")" <&> literal "*" modify imbr10s)
<|> (literal "(" <&> imbrseq <&> sep <&> msequence <&>
literal ")" modify imbr10)
<|> (literal "(" <&> msequence <&> sep <&> imbrseq <&> sep <&>
msequence <&> literal ")" <&> literal "*" modify imbr11s)
<|> (literal "(" <&> msequence <&> sep <&> imbrseq <&> sep <&>
msequence <&> literal ")" modify imbr11)
<|> (msequence <&> sep <&> imbrseq modify imbr12)
<|> (imbrseq <&> sep <&> msequence modify imbr13)) s*)
and lreplicator1 s
= ((range_spec1 <&> literal "[" <&> sep1 <&> literal "|" <&>
concseq1 <&> literal "]" modify lrep1)
<|> (range_spec1 <&> literal "[" <&> sep1 <&> literal "|" <&>
imbrseq1 <&> literal "]" modify lrep2)) s
and rreplicator1 s
= ((range_spec1 <&> literal "[" <&> concseq1 <&> literal "|"
<&> sep1 <&> literal "]" modify rrep1)
<|> (range_spec1 <&> literal "[" <&> imbrseq1 <&> literal "|"
<&> sep1 <&> literal "]" modify rrep2)) s
and integer1 s = (number modify Integer) s
and name111 s = (operation modify Name) s
and mp (p,(a,e)) = Program a
and m_pb1 (a,[]) = Programbody1 a
| m_pb1 (a,[(b)]) = Programbody5 (a,b)
| m_pb1 other = error "impossible"
and m_pb2 (a,[]) = Programbody2 a
| m_pb2 (a,[(b)]) = Programbody6 (a,b)
| m_pb2 other = error "impossible"
and m_pb3 (a,[]) = Programbody3 a
| m_pb3 (a,[(b)]) = Programbody7 (a,b)
| m_pb3 other = error "impossible"
and m_pb4 (a,b) = Programbody4 (a,b)
and mar (a,(b,e)) = Array b
and ar_1 (a,[]) = Arraybody1 a
| ar_1 (a,[(b)]) = Arraybody3 (a,b)
| ar_1 other = error "impossible"
and ar_2 (a,[]) = Arraybody2 a
| ar_2 (a,[(b)]) = Arraybody4 (a,b)
| ar_2 other = error "impossible"
and simp (a,(bra,(b,ket))) = Simpleardecl (a,b)
and more1 (a,[]) = Name1 a
| more1 (a,[(b)]) = Morename (a,b)
| more1 other = error "impossible"
and simp_1 (a,[]) = Simpleardeclbody1 a
| simp_1 (a,[(comma,b)]) = Simpleardeclbody3 (a,b)
| simp_1 other = error "impossible"
and simp_2 (a,(col,(b,[]))) = Simpleardeclbody2 (a,b)
| simp_2 (a,(col,(b,[(comma,c)]))) = Simpleardeclbody4 (a,b,c)
| simp_2 other = error "impossible"
and repl (ra,(sq1,(rep,sq2))) = Replardecl (ra,rep)
and repl_body1 (rep,[]) = Replardeclbody1 rep
| repl_body1 (rep,[(body)]) = Replardeclbody3 (rep,body)
| repl_body1 other = error "impossible"
and repl_body2 (sub,[]) = Replardeclbody2 sub
| repl_body2 (sub,[(body)]) = Replardeclbody4 (sub,body)
| repl_body2 other = error "impossible"
and subs (a,(bra,(b,(ket,[])))) = Subsevents1 (a,b)
| subs (a,(bra,(b,(ket,[(c)])))) = Subsevents2 (a,b,c)
| subs other = error "impossible"
and subs_body (a,[]) = Subseventsbody1 a
| subs_body (a,[(comma,b)]) = Subseventsbody2 (a,b)
| subs_body other = error "impossible"
and range_s (num,(index,(col,(iex1,(com1,(iex2,(com2,iex3)))))))
= Range_spec(index,iex1,iex2,iex3)
and ie_plus (e1,[]) = e1
| ie_plus (e1,[(oper,e2)]) = Plus (e1,e2)
| ie_plus other = error "impossible"
and ie_mul (e1,[]) = e1
| ie_mul (e1,[(oper,e2)]) = Mult (e1,e2)
| ie_mul other = error "impossible"
and ie_div (e1,[]) = e1
| ie_div (e1,[(oper,e2)]) = Div (e1,e2)
| ie_div other = error "impossible"
and ie_pow (e1,[]) = e1
| ie_pow (e1,[(oper,e2)]) = Pow (e1,e2)
| ie_pow other = error "impossible"
and int1 e = Iexpr1 e
and ran e = Iexpr2 e
and ind e = Iexpr3 e
and unparenth (bra,(e,ket)) = Iexpr4 e
and ind_val a = Indexvariable a
and ran_val a = Rangevariable a
and brep (a,(sq1,(b,sq2))) = Bodyreplicator (a,b)
and bbrep1 (a,[]) = BBodyreplicator1 a
| bbrep1 (a,[(b)]) = BBodyreplicator4 (a,b)
| bbrep1 other = error "impossible"
and bbrep2 (a,[]) = BBodyreplicator2 a
| bbrep2 (a,[(b)]) = BBodyreplicator5 (a,b)
| bbrep2 other = error "impossible"
and bbrep3 (a,[]) = BBodyreplicator3 a
| bbrep3 (a,[(b)]) = BBodyreplicator6 (a,b)
| bbrep3 other = error "impossible"
and mpa (p,(b,e)) = Path b
and mpr (p,(b,e)) = Process b
and mseq (a,[]) = Sequence1 a
| mseq (a,[(semicol,b)]) = Sequence2 (a,b)
| mseq other = error "impossible"
and mor (a,[]) = Orelement1 a
| mor (a,[(comma,b)]) = Orelement2 (a,b)
| mor other = error "impossible"
and gel2 (b,[c]) = Gelement5(b,c)
| gel2 (c,[]) = Gelement1(c)
| gel2 other = error "impossible"
and gel2_1 (b,[c]) = Gelement5_1(b,c)
| gel2_1 (c,[]) = Gelement2(c)
| gel2_1 other = error "impossible"
and gel2_2 (b,[c]) = Gelement5_2(b,c)
| gel2_2 (c,[]) = Gelement3(c)
| gel2_2 other = error "impossible"
and ge2 (a,[]) = GelementL1 a
| ge2 (a,[(b)]) = GelementL2(a,b)
| ge2 other = error "impossible"
and gel_4 (a,b) = Gelement4 (a,b)
and mnostar a = Nostar a
and mstar (a,star) = Star a
and meo a = Element a
and mgr (bra,(a,ket)) = Group a
and mev1 (a,[]) = Event2 a
| mev1 (a,[(bra,(b,ket))]) = Event3(a,b)
| mev1 other = error "impossible"
and mev2 (a,(bra,ket)) = Event1 a
and mevb1 (comma,[]) = Empty
| mevb1 (comma,[a]) = Meventbody2 a
| mevb1 other = error "impossible"
and mevb2 (iex,[]) = Meventbody1 iex
| mevb2 (iex,[(comma,[])]) = Meventbody4 iex
| mevb2 (iex,[(comma,[a])]) = Meventbody3 (iex,a)
| mevb2 other = error "impossible"
and dist1 (a,(b,(c,(sq1,(d,sq2))))) = Distributor1 (a,b,c,d)
and dist2 (a,(b,(sq1,(c,sq2)))) = Distributor2 (a,b,c)
and dist3 (a,(b,(sq1,(c,sq2)))) = Distributor3 (a,b,c)
and dist4 (a,(sq1,(b,sq2))) = Distributor4 (a,b)
and dim1 iex = Dim iex
and range1 (nu,(iex1,(co1,(iex2,(co2,iex3)))))
= Range (iex1,iex2,iex3)
and srep1 (ra,(sq1,(c,sq2))) = Sreplicator1 (ra,c)
and srep2 (ra,(sq1,(i,sq2))) = Sreplicator2 (ra,i)
and cons (a,(b,at)) = Concseq (a,b)
and imbr1 (mseq1,(sep1,(at1,(sep2,(at2,(sep3,mseq2))))))
= Imbrseq1 (mseq1,sep1,sep2,sep3,mseq2)
and imbr2 (mseq1,(sep1,(at1,(sep2,(mseq2,(sep3,
(at2,(sep4,mseq3))))))))
= Imbrseq2 (mseq1,sep1,sep2,mseq2,sep3,sep4,mseq3)
and imbr3 (bra,(at1,(at2,(sep1,(mseq1,ket)))))
= Imbrseq3 (sep1,mseq1)
and imbr3s (bra,(at1,(at2,(sep1,(mseq1,(ket,st))))))
= Imbrseq3s (sep1,mseq1)
and imbr4 (bra,(at1,(mseq1,(sep1,(at2,(sep2,(mseq2,ket)))))))
= Imbrseq4 (mseq1,sep1,sep2,mseq2)
and imbr4s (bra,(at1,(mseq1,(sep1,(at2,(sep2,
(mseq2,(ket,st))))))))
= Imbrseq4s (mseq1,sep1,sep2,mseq2)
and imbr5 (bra,(mseq1,(sep1,(at1,(at2,ket)))))
= Imbrseq5 (mseq1,sep1)
and imbr5s (bra,(mseq1,(sep1,(at1,(at2,(ket,st))))))
= Imbrseq5s (mseq1,sep1)
and imbr6 (bra,(mseq1,(sep1,(at1,(sep2,(mseq2,(at2,ket)))))))
= Imbrseq6 (mseq1,sep1,sep2,mseq2)
and imbr6s (bra,(mseq1,(sep1,(at1,(sep2,(mseq2,
(at2,(ket,st))))))))
= Imbrseq6s (mseq1,sep1,sep2,mseq2)
and imbr7 (bra,(at1,(mseq1,(at2,ket)))) = Imbrseq7 mseq1
and imbr7s (bra,(at1,(mseq1,(at2,ket)))) = Imbrseq7s mseq1
and imbr8 (bra,(imb,ket)) = Imbrseq8 imb
and imbr8s (bra,(imb,(ket,st))) = Imbrseq8s imb
(*and imbr9 (bra,(mseq1,(sep1,(imb,ket))))
= Imbrseq9 (mseq1,sep1,imb)
and imbr9s (bra,(mseq1,(sep1,(imb,(ket,st)))))
= Imbrseq9s (mseq1,sep1,imb)
and imbr10 (bra,(imb,(sep1,(mseq1,ket))))
= Imbrseq10 (imb,sep1,mseq1)
and imbr10s (bra,(imb,(sep1,(mseq1,(ket,st)))))
= Imbrseq10s (imb,sep1,mseq1)
and imbr11 (bra,(mseq1,(sep1,(imb,(sep2,(mseq2,ket))))))
= Imbrseq11 (mseq1,sep1,imb,sep2,mseq2)
and imbr11s (bra,(mseq1,(sep1,(imb,(sep2,(mseq2,(ket,st)))))))
= Imbrseq11s (mseq1,sep1,imb,sep2,mseq2)
and imbr12 (mseq1,(sep1,imb)) = Imbrseq12 (mseq1,sep1,imb)
and imbr13 (imb,(sep1,mseq1)) = Imbrseq13 (imb,sep1,mseq1)*)
and lrep1 (ra,(sq1,(s,(bar,(c,sq2))))) = Lreplicator1 (ra,s,c)
and lrep2 (ra,(sq1,(s,(bar,(i,sq2))))) = Lreplicator2 (ra,s,i)
and rrep1 (ra,(sq1,(c,(bar,(s,sq2))))) = Rreplicator1 (ra,c,s)
and rrep2 (ra,(sq1,(i,(bar,(s,sq2))))) = Rreplicator2 (ra,i,s)
in
fun m_parser x = mprogram1 x
end
end
(* end of file `nmp_parser.sml' *)
(* File name: csr_prelude.sml
Objective: This file contains functions that are used frequently
in checking Context-Sensitive Restrictions *)
functor Csr_prelude(structure CSY: COSY
structure LX: LEX
structure PRLD: PRELUDE): CSR_PRELUDE =
struct
structure CSY = CSY
structure PRLD = PRLD
structure LX = LX
open CSY
open PRLD
open LX
val unboundlist = ref [{name=" ", value=0}]
type unbound = {name : string,
value : int}
fun iex1 (Dim(a)) = iex a
and iex (Iexpr1(Integer a)) = a
| iex (Iexpr2(Rangevariable(Name a)))
= getvalue(a,(!unboundlist))
| iex (Plus(a,b)) = (iex a) + (iex b)
| iex (Mult(a,b)) = (iex a) * (iex b)
| iex (Div(a,b)) = (iex a) div (iex b)
| iex (Pow(a,b)) = power((iex a),(iex b))
| iex (Iexpr4(a)) = iex a
| iex other = error "imposible" handle Error => 0
and power(a,b) = if b>1 then a * power(a,(b-1)) else a
(* get the corresponding value from unbound list *)
and getvalue(a,((l:unbound)::x))
= if a = (#name l) then (#value l) else getvalue(a,x)
| getvalue(a,[]) = cr_unbound_list(a,unboundlist)
(* create unbound list and read the value from keyboard and
return the value *)
and cr_unbound_list(a,unboundlist)
= let val read_value = inp a
in unboundlist := (!unboundlist) @ [{name=a, value=read_value}];
read_value
end
(* input integer from keyboard *)
and inp (msg:string)
= (print ("Please input the INTEGER value of " ^ msg ^ ": ");
inp1(lexanal(explode(input_line(std_in))),msg))
and inp1 ([Number a],msg) = a
| inp1 (other,msg) = error "Error !!!" handle Error => inp msg
end
(* end of file `csr_prelude.sml' *)
(* File name: csr.sml
Objective: Checks if the COSY program satisfies the Context-
Sensitive Restrictions given in [JL92]pp.460-461.
Eech restriction has its own program.
Input : mprogram (tree)
Output : bool *)
functor Csr(structure CSY: COSY
structure CSR_PRLD: CSR_PRELUDE
structure PRLD: PRELUDE
sharing CSR_PRLD.CSY = CSY ): CSR =
struct
structure CSY = CSY
structure CSR_PRLD = CSR_PRLD
structure PRLD = PRLD
val err_cnt = ref 0;
type bound = {pos : int,
lower : int,
upper : int,
step : int}
type Arraytable = {name : string,
dim : int,
value : bound list}
type unbound = {name : string,
value : int}
(* checks if the y is array name or not *)
fun mem ((a:Arraytable)::x,y)
= if (y=(#name a)) then true else mem(x,y)
| mem ([],y) = false
(* The following program which is between the 'local' and 'end'
is used to create an array table which stores all the array
names, dimensions and their bounds.
Input : mprogram (tree)
Output : Arraytable *)
local
open CSY
open CSR_PRLD
open PRLD
type temp = {n1 : string,
lower : int,
upper : int,
step : int};
fun mkt (Program(a)) = mpbody a
and mpbody (Programbody4(a,b)) = (arr a) @ (mpbody b)
| mpbody (Programbody5(a,b)) = mpbody b
| mpbody (Programbody6(a,b)) = mpbody b
| mpbody (Programbody7(a,b)) = mpbody b
| mpbody other = []
and arr (Array(a)) = arbody a
and arbody (Arraybody1(a)) = sardecl a
| arbody (Arraybody2(a)) = rardecl a []
| arbody (Arraybody3(a,b)) = (sardecl a) @ (arbody b)
| arbody (Arraybody4(a,b)) = (rardecl a []) @ (arbody b)
and sardecl (Simpleardecl(a,b))
= mname a (count1 b) (range1 b 1)
(* function "count1" counts the number of dimention *)
and count1 (Simpleardeclbody1(a)) = 1
| count1 (Simpleardeclbody3(a,b)) = 1 + count1(b)
| count1 (Simpleardeclbody2(a,b)) = 1
| count1 (Simpleardeclbody4(a,b,c)) = 1 + count1(c)
and range1 (Simpleardeclbody1(a)) num
= [{pos=num, lower=1, upper=iex a, step=1}]
| range1 (Simpleardeclbody3(a,b)) num
= [{pos=num, lower=1, upper=iex a, step=1}] @
(range1 b (num+1))
| range1 (Simpleardeclbody2(a,b)) num
= [{pos=num, lower=iex a, upper=iex b, step=1}]
| range1 (Simpleardeclbody4(a,b,c)) num
= [{pos=num, lower=iex a, upper=iex b, step=1}]
@ (range1 c (num+1))
and iex2 (Iexpr2(Rangevariable(Name a))) ((h:temp)::x)
= if a = (#n1 h) then true
else iex2 (Iexpr2(Rangevariable(Name a))) x
| iex2 other l = false
and iex3 (Iexpr2(Rangevariable(Name a))) ((h:temp)::x)
= if a = (#n1 h) then (#lower h)
else iex3 (Iexpr2(Rangevariable(Name a))) x
| iex3 other l = 0
and rardecl (Replardecl(a,b)) l
= rardeclbody b ((range2 a l) @ l)
and rardeclbody (Replardeclbody1(a)) r1 = rardecl a r1
| rardeclbody (Replardeclbody2(a)) r1 = se a r1 1
| rardeclbody (Replardeclbody3(a,b)) r1
= (rardecl a r1) @ (rardeclbody b r1)
| rardeclbody (Replardeclbody4(a,b)) r1
= (se a r1 1) @ (rardeclbody b r1)
and se (Subsevents1(a,b)) r1 num
= mname a (count2 b) (range3 b r1 num)
| se (Subsevents2(a,b,c)) r1 num
= (mname a (count2 b) (range3 b r1 num)) @ (se c r1 num)
(* function "count2" counts the number of dimention *)
and count2 (Subseventsbody1(a)) = 1
| count2 (Subseventsbody2(a,b)) = 1 + count2(b)
(* function "range2" creates a temp list of the index range. *)
and range2 (Range_spec(a,b,c,d)) l
= if iex2 c l
then mklist (ivar a,iex b,iex d,(iex3 c l),l,(otherdim c l))
else [{n1=ivar a,lower=iex b, upper=iex c, step=iex d}]
(* function otherdim uses to get the value from other dimension *)
and otherdim (Iexpr2(Rangevariable(Name a))) ((h:temp)::x)
= if a = (#n1 h) then {n1=(#n1 h),
lower=(#lower h),
upper=(#upper h),
step=(#step h)
}
else otherdim (Iexpr2(Rangevariable(Name a))) x
| otherdim other l = error "impossible"
and mklist (a,b,c,d,l,l1)
= if d <= (#upper l1)
then [{n1=a, lower=b, upper=d, step=c}]
@ (mklist (a,b,c,(d+(#step l1)),l,l1))
else []
(* function "range3" creates a list of the index range *)
and range3 (Subseventsbody1(Iexpr2(Rangevariable(Name a))))
((h:temp)::x) num
= if a = (#n1 h)
then [{pos=num,lower=(#lower h),upper=(#upper h),
step=(#step h)}]
@ range3 (Subseventsbody1(Iexpr2
(Rangevariable(Name a)))) x num
else range3 (Subseventsbody1(Iexpr2
(Rangevariable(Name a)))) x num
| range3 (Subseventsbody2(Iexpr2(Rangevariable(Name a)),b))
((h:temp)::x) num
= (if a = (#n1 h)
then [{pos=num,lower=(#lower h),upper=(#upper h),
step=(#step h)}]
@ range3 (Subseventsbody1(Iexpr2
(Rangevariable(Name a)))) x num
else (range3 (Subseventsbody1(Iexpr2
(Rangevariable(Name a)))))
x num) @ (range3 b (h::x) (num+1))
| range3 other (h::x) num = error "imposible"
| range3 other [] num = []
and ivar(Indexvariable(Name a)) = a
and mname (Name1(a)) k r = na a k r
| mname (Morename(a,b)) k r = (na a k r) @ (mname b k r)
and na (Name b) k r = [{name = b, dim = k, value = r}]
in
fun mktbl x = mkt x
end
(* The following program which is between the 'local' and 'end'
is used to check if the COSY program satisfies Crest1.
Crest1: If the upperbound and lowerbound of dimensions of the
collective names are integers then the upperbound has
to be greater then or equal to their corresponding
implicit or explicit lowerbound. *)
local
open CSY
open CSR_PRLD
open PRLD
fun cres1 ((a:Arraytable)::x)
= if (cres11 (#value a)) then cres1 x
else (error ("Array '" ^ (#name a) ^
"': upperbound is smaller then lowerbound.")
handle Error => (err_cnt:=(!err_cnt)+1; cres1 x))
| cres1 [] = true
and cres11 ((b:bound)::y)
= if ((#lower b) > (#upper b)) andalso ((#step b) > 0)
then false else cres11 y
| cres11 [] = true
in
fun crest1 x = cres1 (mktbl x)
end;
(* The following program which is between the 'local' and 'end'
is used to check if the COSY program satisfies Crest2.
Crest2: An array identifier may occur only once in
collectivisors. *)
local
open CSY
open CSR_PRLD
open PRLD
fun cres2 ((a:Arraytable)::x) l
= if member l (#name a)
then error ("The identifier '" ^ (#name a)
^ "' is duplicate")
handle Error => (err_cnt:=((!err_cnt) + 1); cres2 x l)
else cres2 x (l @ [#name a])
| cres2 [] l = true
in
fun crest2 x = cres2 (mktbl x) []
end;
(* The following program which is between the 'local' and 'end'
is used to check if the COSY program satisfies Crest3.
Crest3: Each replicator without range variables must specify
a non empty range for its index. *)
local
open CSY
open CSR_PRLD
open PRLD
fun cres3 (Program(a)) = mpbody a
and mpbody (Programbody4(a,b)) = (arr a) andalso (mpbody b)
| mpbody (Programbody5(a,b)) = mpbody b
| mpbody (Programbody6(a,b)) = mpbody b
| mpbody (Programbody7(a,b)) = mpbody b
| mpbody other = true
and arr (Array(a)) = arbody a
and arbody (Arraybody2(a)) = rardecl a
| arbody (Arraybody3(a,b)) = arbody b
| arbody (Arraybody4(a,b)) = (rardecl a) andalso (arbody b)
| arbody other = true
and rardecl (Replardecl(a,b)) = ran a
and ran (Range_spec(a,b,c,d)) =
if (((iex c) - (iex b) > 0) andalso ((iex d) < 0)) orelse
(((iex c) - (iex b) < 0) andalso ((iex d) > 0))
then error "The range is empty"
handle Error => (err_cnt := (!err_cnt) + 1; true)
else true
in
fun crest3 x = cres3 x
end;
(* The following program which is between the 'local' and 'end'
is used to check if the COSY program satisfies Irest1.
Irest1: Identifiers for replicator indices and range variables
should be distinct from any identifiers used for simple
events. Identifiers for replicator indices and range
variables should also be distinct.*)
local
open CSY
open CSR_PRLD
open PRLD
(* remove redundant elements in the list *)
fun Rredundant (a::x) l = if member l a then Rredundant x l
else Rredundant x (l @ [a])
| Rredundant [] l = l
local (* create a list of index variables *)
fun indvarlist (Program(a)) = mpbody a
and mpbody (Programbody1(a)) = mpa a
| mpbody (Programbody2(a)) = mpr a
| mpbody (Programbody3(a)) = brep a
| mpbody (Programbody4(a,b)) = (arr a) @ (mpbody b)
| mpbody (Programbody5(a,b)) = (mpa a) @ (mpbody b)
| mpbody (Programbody6(a,b)) = (mpr a) @ (mpbody b)
| mpbody (Programbody7(a,b)) = (brep a) @ (mpbody b)
and arr (Array(a)) = arbody a
and arbody (Arraybody2(a)) = rardecl a
| arbody (Arraybody3(a,b)) = arbody b
| arbody (Arraybody4(a,b)) = (rardecl a) @ (arbody b)
| arbody other = []
and rardecl (Replardecl(a,b)) = (ran a) @ (rardeclbody b)
and rardeclbody (Replardeclbody1(a)) = rardecl a
| rardeclbody (Replardeclbody3(a,b))
= (rardecl a) @ (rardeclbody b)
| rardeclbody (Replardeclbody4(a,b)) = rardeclbody b
| rardeclbody other = []
and ran (Range_spec(a,b,c,d))
= (ind a) @ (iex1 b (ind a)) @ (iex1 c (ind a))
@ (iex1 d (ind a))
and ind (Indexvariable(a)) = na a
and mpa (Path(a)) = mseq a
and mpr (Process(a)) = mseq a
and brep (Bodyreplicator(a,b)) = (ran a) @ (bbrep b)
and bbrep (BBodyreplicator1(a)) = mpa a
| bbrep (BBodyreplicator2(a)) = mpr a
| bbrep (BBodyreplicator3(a)) = brep a
| bbrep (BBodyreplicator4(a,b)) = (mpa a) @ (bbrep b)
| bbrep (BBodyreplicator5(a,b)) = (mpr a) @ (bbrep b)
| bbrep (BBodyreplicator6(a,b)) = (brep a) @ (bbrep b)
and mseq (Sequence1(a)) = morel a
| mseq (Sequence2(a,b)) = (morel a) @ (mseq b)
and morel (Orelement1(a)) = mgel a
| morel (Orelement2(a,b)) = (mgel a ) @ (morel b )
and mgel (Gelement1(a)) = mstel a
| mgel (Gelement2(a)) = srepl a
| mgel (Gelement4(a,b)) = (rrepl a) @ (mgel b)
| mgel (Gelement5(a,b)) = (mstel a) @ (mgelL b)
| mgel (Gelement5_1(a,b)) = (srepl a) @ (mgelL b)
| mgel (Gelement5_2(a,b)) = (mgelL b)
| mgel other = []
and mgelL (GelementL1(a)) = lrepl a
| mgelL (GelementL2(a,b)) = (lrepl a) @ (mgelL b)
and srepl (Sreplicator1(a,b)) = (ran a) @ (conc b)
| srepl (Sreplicator2(a,b)) = (ran a) @ (imbr b)
and conc (Concseq(a,b)) = mseq a
and imbr (Imbrseq1(a,b,c,d,e)) = (mseq a) @ (mseq e)
| imbr (Imbrseq2(a,b,c,d,e,f,g))
= (mseq a) @ (mseq d) @ (mseq g)
| imbr (Imbrseq3(a,b)) = mseq b
| imbr (Imbrseq3s(a,b)) = mseq b
| imbr (Imbrseq4(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq4s(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq5(a,b)) = mseq a
| imbr (Imbrseq5s(a,b)) = mseq a
| imbr (Imbrseq6(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq6s(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq7(a)) = mseq a
| imbr (Imbrseq7s(a)) = mseq a
| imbr (Imbrseq8(a)) = imbr a
| imbr (Imbrseq8s(a)) = imbr a
(*| imbr (Imbrseq9(a,b,c)) = (mseq a) @ (imbr c)
| imbr (Imbrseq9s(a,b,c)) = (mseq a) @ (imbr c)
| imbr (Imbrseq10(a,b,c)) = (imbr a) @ (mseq c)
| imbr (Imbrseq10s(a,b,c)) = (imbr a) @ (mseq c)
| imbr (Imbrseq11(a,b,c,d,e))
= (mseq a) @ (imbr c) @ (mseq e)
| imbr (Imbrseq11s(a,b,c,d,e))
= (mseq a) @ (imbr c) @ (mseq e)
| imbr (Imbrseq12(a,b,c)) = (mseq a) @ (imbr c)
| imbr (Imbrseq13(a,b,c)) = (imbr a) @ (mseq c)*)
and rrepl (Rreplicator1(a,b,c)) = (ran a) @ (conc b)
| rrepl (Rreplicator2(a,b,c)) = (ran a) @ (imbr b)
and lrepl (Lreplicator1(a,b,c)) = (ran a) @ (conc c)
| lrepl (Lreplicator2(a,b,c)) = (ran a) @ (imbr c)
and mstel (Nostar(a)) = mel a
| mstel (Star(a)) = mel a
and mel (Group(a)) = mseq a
| mel other = []
and na (Name(a)) = [a]
and iex1 (Iexpr2(Rangevariable(Name a))) b
= if member b a then
error "same index name within the same range"
handle Error => (err_cnt := (!err_cnt) + 1; [])
else []
| iex1 other b = []
in
fun Rrdt1 x = Rredundant (indvarlist x) []
end
local (* create a list of events *)
fun evlist (Program(a)) = mpbody a
and mpbody (Programbody1(a)) = mpa a
| mpbody (Programbody2(a)) = mpr a
| mpbody (Programbody3(a)) = brep a
| mpbody (Programbody4(a,b)) = (arr a) @ (mpbody b)
| mpbody (Programbody5(a,b)) = (mpa a) @ (mpbody b)
| mpbody (Programbody6(a,b)) = (mpr a) @ (mpbody b)
| mpbody (Programbody7(a,b)) = (brep a) @ (mpbody b)
and arr (Array(a)) = arbody a
and arbody (Arraybody1(a)) = sardecl a
| arbody (Arraybody2(a)) = rardecl a
| arbody (Arraybody3(a,b)) = (sardecl a) @ (arbody b)
| arbody (Arraybody4(a,b)) = (rardecl a) @ (arbody b)
and sardecl (Simpleardecl(a,b)) = mname a
and rardecl (Replardecl(a,b)) = rardeclbody b
and rardeclbody (Replardeclbody1(a)) = rardecl a
| rardeclbody (Replardeclbody2(a)) = subs a
| rardeclbody (Replardeclbody3(a,b))
= (rardecl a) @ (rardeclbody b)
| rardeclbody (Replardeclbody4(a,b))
= (subs a) @ (rardeclbody b)
and subs (Subsevents1(a,b)) = mname a
| subs (Subsevents2(a,b,c)) = (mname a) @ (subs c)
and mpa (Path(a)) = mseq a
and mpr (Process(a)) = mseq a
and brep (Bodyreplicator(a,b)) = bbrep b
and bbrep (BBodyreplicator1(a)) = mpa a
| bbrep (BBodyreplicator2(a)) = mpr a
| bbrep (BBodyreplicator3(a)) = brep a
| bbrep (BBodyreplicator4(a,b)) = (mpa a) @ (bbrep b)
| bbrep (BBodyreplicator5(a,b)) = (mpr a) @ (bbrep b)
| bbrep (BBodyreplicator6(a,b)) = (brep a) @ (bbrep b)
and mseq (Sequence1(a)) = morel a
| mseq (Sequence2(a,b)) = (morel a) @ (mseq b)
and morel (Orelement1(a)) = mgel a
| morel (Orelement2(a,b)) = (mgel a ) @ (morel b )
and mgel (Gelement1(a)) = mstel a
| mgel (Gelement2(a)) = srepl a
| mgel (Gelement3(a)) = dist a
| mgel (Gelement4(a,b)) = (rrepl a) @ (mgel b)
| mgel (Gelement5(a,b)) = (mstel a) @ (mgelL b)
| mgel (Gelement5_1(a,b)) = (srepl a) @ (mgelL b)
| mgel (Gelement5_2(a,b)) = (dist a) @ (mgelL b)
and mgelL (GelementL1(a)) = lrepl a
| mgelL (GelementL2(a,b)) = (lrepl a) @ (mgelL b)
and srepl (Sreplicator1(a,b)) = conc b
| srepl (Sreplicator2(a,b)) = imbr b
and dist (Distributor1(a,b,c,d)) = mseq d
| dist (Distributor2(a,b,c)) = mseq c
| dist (Distributor3(a,b,c)) = mseq c
| dist (Distributor4(a,b)) = mseq b
and rrepl (Rreplicator1(a,b,c)) = conc b
| rrepl (Rreplicator2(a,b,c)) = imbr b
and lrepl (Lreplicator1(a,b,c)) = conc c
| lrepl (Lreplicator2(a,b,c)) = imbr c
and conc (Concseq(a,b)) = mseq a
and imbr (Imbrseq1(a,b,c,d,e)) = (mseq a) @ (mseq e)
| imbr (Imbrseq2(a,b,c,d,e,f,g))
= (mseq a) @ (mseq d) @ (mseq g)
| imbr (Imbrseq3(a,b)) = mseq b
| imbr (Imbrseq3s(a,b)) = mseq b
| imbr (Imbrseq4(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq4s(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq5(a,b)) = mseq a
| imbr (Imbrseq5s(a,b)) = mseq a
| imbr (Imbrseq6(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq6s(a,b,c,d)) = (mseq a) @ (mseq d)
| imbr (Imbrseq7(a)) = mseq a
| imbr (Imbrseq7s(a)) = mseq a
| imbr (Imbrseq8(a)) = imbr a
| imbr (Imbrseq8s(a)) = imbr a
(*| imbr (Imbrseq9(a,b,c)) = (mseq a) @ (imbr c)
| imbr (Imbrseq9s(a,b,c)) = (mseq a) @ (imbr c)
| imbr (Imbrseq10(a,b,c)) = (imbr a) @ (mseq c)
| imbr (Imbrseq10s(a,b,c)) = (imbr a) @ (mseq c)
| imbr (Imbrseq11(a,b,c,d,e))
= (mseq a) @ (imbr c) @ (mseq e)
| imbr (Imbrseq11s(a,b,c,d,e))
= (mseq a) @ (imbr c) @ (mseq e)
| imbr (Imbrseq12(a,b,c)) = (mseq a) @ (imbr c)
| imbr (Imbrseq13(a,b,c)) = (imbr a) @ (mseq c)*)
and mstel (Nostar(a)) = mel a
| mstel (Star(a)) = mel a
and mel (Element(a)) = mev a
| mel (Group(a)) = mseq a
and mev (Event1(a)) = na a
| mev (Event2(a)) = na a
| mev (Event3(a,b)) = na a
and mname (Name1(a)) = na a
| mname (Morename(a,b)) = (na a) @ (mname b)
and na (Name(a)) = [a]
in
fun Rrdt2 x = Rredundant (evlist x) []
end
fun ires1 (x,b::y) = if member x b then error
"the index and range variable are using the same name"
handle Error => (err_cnt := (!err_cnt) + 1; true)
else ires1 (x,y)
| ires1 other = true
in
fun irest1 x = ires1 ((Rrdt1 x),(Rrdt2 x))
end
(* The following program which is between the 'local' and 'end'
is used to check if the COSY program satisfies Irest2.
Irest2: Replicator index variables are only defined inside the
[] of the replicators with which they are associated.
In the scope of a replicator index variable no other
replicator index variable having the same name is
permitted. *)
local
open CSY
open CSR_PRLD
open PRLD
fun ires2 (Program(a)) = mpbody a 1 1
and mpbody (Programbody1(a)) pnum cnum = mpa a [] pnum
| mpbody (Programbody2(a)) pnum cnum = mpr a [] pnum
| mpbody (Programbody3(a)) pnum cnum = brep a [] pnum
| mpbody (Programbody4(a,b)) pnum cnum
= (arr a cnum) andalso (mpbody b pnum (cnum+1))
| mpbody (Programbody5(a,b)) pnum cnum
= (mpa a [] pnum) andalso (mpbody b (pnum+1) cnum)
| mpbody (Programbody6(a,b)) pnum cnum
= (mpr a [] pnum) andalso (mpbody b (pnum+1) cnum)
| mpbody (Programbody7(a,b)) pnum cnum
= (brep a [] pnum) andalso (mpbody b (pnum+1) cnum)
and arr (Array(a)) cnum = arbody a cnum
and arbody (Arraybody2(a)) cnum = rardecl a [] cnum
| arbody (Arraybody3(a,b)) cnum = arbody b cnum
| arbody (Arraybody4(a,b)) cnum
= (rardecl a [] cnum) andalso (arbody b cnum)
| arbody other cnum = true
and rardecl (Replardecl(a,b)) l cnum
= rardeclbody b (ran a l cnum) cnum
and rardeclbody (Replardeclbody1(a)) l cnum = rardecl a l cnum
| rardeclbody (Replardeclbody3(a,b)) l cnum
= (rardecl a l cnum) andalso (rardeclbody b l cnum)
| rardeclbody (Replardeclbody4(a,b)) l cnum
= rardeclbody b l cnum
| rardeclbody other l cnum = true
and ran (Range_spec(a,b,c,d)) l cnum = ind a l cnum
and ind (Indexvariable(Name a)) l cnum
= if member l a then
(error ("C"^stringofint(cnum)^": Duplicate index variable")
handle Error => (err_cnt := (!err_cnt) + 1; []))
else (l @ [a])
and ran1 (Range_spec(a,b,c,d)) l pnum = ind1 a l pnum
and ind1 (Indexvariable(Name a)) l pnum
= if member l a then
(error ("C"^stringofint(pnum)^": Duplicate index variable")
handle Error => (err_cnt := (!err_cnt) + 1; []))
else (l @ [a])
and mpa (Path(a)) l pnum = mseq a l pnum
and mpr (Process(a)) l pnum = mseq a l pnum
and brep (Bodyreplicator(a,b)) l pnum
= bbrep b (ran1 a l pnum) pnum
and bbrep (BBodyreplicator1(a)) l pnum = mpa a l pnum
| bbrep (BBodyreplicator2(a)) l pnum = mpr a l pnum
| bbrep (BBodyreplicator3(a)) l pnum = brep a l pnum
| bbrep (BBodyreplicator4(a,b)) l pnum
= (mpa a l pnum) andalso (bbrep b l pnum)
| bbrep (BBodyreplicator5(a,b)) l pnum
= (mpr a l pnum) andalso (bbrep b l pnum)
| bbrep (BBodyreplicator6(a,b)) l pnum
= (brep a l pnum) andalso (bbrep b l pnum)
and mseq (Sequence1(a)) l pnum = morel a l pnum
| mseq (Sequence2(a,b)) l pnum
= (morel a l pnum) andalso (mseq b l pnum)
and morel (Orelement1(a)) l pnum = mgel a l pnum
| morel (Orelement2(a,b)) l pnum
= (mgel a l pnum) andalso (morel b l pnum)
and mgel (Gelement1(a)) l pnum = mstel a l pnum
| mgel (Gelement2(a)) l pnum = srepl a l pnum
| mgel (Gelement4(a,b)) l pnum
= (rrepl a l pnum) andalso (mgel b l pnum)
| mgel (Gelement5(a,b)) l pnum
= (mstel a l pnum) andalso (mgelL b l pnum)
| mgel (Gelement5_1(a,b)) l pnum
= (srepl a l pnum) andalso (mgelL b l pnum)
| mgel (Gelement5_2(a,b)) l pnum = (mgelL b l pnum)
| mgel other l pnum = true
and mgelL (GelementL1(a)) l pnum = lrepl a l pnum
| mgelL (GelementL2(a,b)) l pnum
= (lrepl a l pnum) andalso (mgelL b l pnum)
and srepl (Sreplicator1(a,b)) l pnum
= conc b (ran1 a l pnum) pnum
| srepl (Sreplicator2(a,b)) l pnum
= imbr b (ran1 a l pnum) pnum
and conc (Concseq(a,b)) l pnum = mseq a l pnum
and imbr (Imbrseq1(a,b,c,d,e)) l pnum
= (mseq a l pnum) andalso (mseq e l pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) l pnum
= (mseq a l pnum) andalso (mseq d l pnum) andalso
(mseq g l pnum)
| imbr (Imbrseq3(a,b)) l pnum = mseq b l pnum
| imbr (Imbrseq3s(a,b)) l pnum = mseq b l pnum
| imbr (Imbrseq4(a,b,c,d)) l pnum
= (mseq a l pnum) andalso (mseq d l pnum)
| imbr (Imbrseq4s(a,b,c,d)) l pnum
= (mseq a l pnum) andalso (mseq d l pnum)
| imbr (Imbrseq5(a,b)) l pnum = mseq a l pnum
| imbr (Imbrseq5s(a,b)) l pnum = mseq a l pnum
| imbr (Imbrseq6(a,b,c,d)) l pnum
= (mseq a l pnum) andalso (mseq d l pnum)
| imbr (Imbrseq6s(a,b,c,d)) l pnum
= (mseq a l pnum) andalso (mseq d l pnum)
| imbr (Imbrseq7(a)) l pnum = mseq a l pnum
| imbr (Imbrseq7s(a)) l pnum = mseq a l pnum
| imbr (Imbrseq8(a)) l pnum = imbr a l pnum
| imbr (Imbrseq8s(a)) l pnum = imbr a l pnum
(*| imbr (Imbrseq9(a,b,c)) l = (mseq a l) andalso (imbr c l)
| imbr (Imbrseq9s(a,b,c)) l = (mseq a l) andalso (imbr c l)
| imbr (Imbrseq10(a,b,c)) l = (imbr a l) andalso (mseq c l)
| imbr (Imbrseq10s(a,b,c)) l = (imbr a l) andalso (mseq c l)
| imbr (Imbrseq11(a,b,c,d,e)) l
= (mseq a l) andalso (imbr c l) andalso (mseq e l)
| imbr (Imbrseq11s(a,b,c,d,e)) l
= (mseq a l) andalso (imbr c l) andalso (mseq e l)
| imbr (Imbrseq12(a,b,c)) l = (mseq a l) andalso (imbr c l)
| imbr (Imbrseq13(a,b,c)) l = (imbr a l) andalso (mseq c l)*)
and rrepl (Rreplicator1(a,b,c)) l pnum
= conc b (ran1 a l pnum) pnum
| rrepl (Rreplicator2(a,b,c)) l pnum
= imbr b (ran1 a l pnum) pnum
and lrepl (Lreplicator1(a,b,c)) l pnum
= conc c (ran1 a l pnum) pnum
| lrepl (Lreplicator2(a,b,c)) l pnum
= imbr c (ran1 a l pnum) pnum
and mstel (Nostar(a)) l pnum = mel a l pnum
| mstel (Star(a)) l pnum = mel a l pnum
and mel (Group(a)) l pnum = mseq a l pnum
| mel (Element(a)) l pnum = mev a l pnum
and mev (Event3(a,b)) l pnum = mevb b l pnum
| mev other l pnum = true
and mevb (Meventbody1(a)) l pnum = chk a l pnum
| mevb (Empty) l pnum = true
| mevb (Meventbody2(a)) l pnum = mevb a l pnum
| mevb (Meventbody3(a,b)) l pnum
= (chk a l pnum) andalso (mevb b l pnum)
| mevb (Meventbody4(a)) l pnum = chk a l pnum
and chk (Iexpr2(Rangevariable(Name(a)))) l pnum
= if member l a then true
else (error ("P"^stringofint(pnum)
^": Use index variable outside the []")
handle Error => (err_cnt := (!err_cnt) + 1; true))
| chk other l pnum = true
in
fun irest2 x = ires2 x
end
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the BRrest.
BRrest: The range of the bodyreplicator indices should be
non-empty. *)
local
open CSY
open CSR_PRLD
open PRLD
fun brest (Program(a)) = mpbody a 1
and mpbody (Programbody3(a)) pnum = brep a pnum
| mpbody (Programbody4(a,b)) pnum = mpbody b pnum
| mpbody (Programbody5(a,b)) pnum = mpbody b (pnum+1)
| mpbody (Programbody6(a,b)) pnum = mpbody b (pnum+1)
| mpbody (Programbody7(a,b)) pnum
= (brep a pnum) andalso (mpbody b (pnum+1))
| mpbody other pnum = true
and brep (Bodyreplicator(a,b)) pnum = ran a pnum
and ran (Range_spec(a,b,c,d)) pnum =
if (((iex c) - (iex b) > 0) andalso ((iex d) < 0)) orelse
(((iex c) - (iex b) < 0) andalso ((iex d) > 0))
then (error ("P"^stringofint(pnum)
^": The range of the bodyreplicator indices is empty")
handle Error => (err_cnt:=(!err_cnt)+1; true))
else true
in
fun brrest x = brest x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Rrest1.1.
Rrest1.1: For every replicator if inc is an integer then inc<>0.*)
local
open CSY
open CSR_PRLD
open PRLD
fun rres11 (Program(a)) = mpbody a 1 1
and mpbody (Programbody1(a)) pnum cnum = mpa a pnum
| mpbody (Programbody2(a)) pnum cnum = mpr a pnum
| mpbody (Programbody3(a)) pnum cnum = brep a pnum
| mpbody (Programbody4(a,b)) pnum cnum
= (arr a cnum) andalso (mpbody b pnum (cnum+1))
| mpbody (Programbody5(a,b)) pnum cnum
= (mpa a pnum) andalso (mpbody b (pnum+1) cnum)
| mpbody (Programbody6(a,b)) pnum cnum
= (mpr a pnum) andalso (mpbody b (pnum+1) cnum)
| mpbody (Programbody7(a,b)) pnum cnum
= (brep a pnum) andalso (mpbody b (pnum+1) cnum)
and arr (Array(a)) cnum = arbody a cnum
and arbody (Arraybody2(a)) cnum = rardecl a cnum
| arbody (Arraybody3(a,b)) cnum = arbody b cnum
| arbody (Arraybody4(a,b)) cnum
= (rardecl a cnum) andalso (arbody b cnum)
| arbody other cnum = true
and rardecl (Replardecl(a,b)) cnum
= (ran1 a cnum) andalso (rardeclbody b cnum)
and rardeclbody (Replardeclbody1(a)) cnum = rardecl a cnum
| rardeclbody (Replardeclbody3(a,b)) cnum
= (rardecl a cnum) andalso (rardeclbody b cnum)
| rardeclbody (Replardeclbody4(a,b)) cnum = rardeclbody b cnum
| rardeclbody other cnum = true
and mpa (Path(a)) pnum = mseq a pnum
and mpr (Process(a)) pnum = mseq a pnum
and brep (Bodyreplicator(a,b)) pnum
= (ran a pnum) andalso (bbrep b pnum)
and bbrep (BBodyreplicator1(a)) pnum = mpa a pnum
| bbrep (BBodyreplicator2(a)) pnum = mpr a pnum
| bbrep (BBodyreplicator3(a)) pnum = brep a pnum
| bbrep (BBodyreplicator4(a,b)) pnum
= (mpa a pnum) andalso (bbrep b pnum)
| bbrep (BBodyreplicator5(a,b)) pnum
= (mpr a pnum) andalso (bbrep b pnum)
| bbrep (BBodyreplicator6(a,b)) pnum
= (brep a pnum) andalso (bbrep b pnum)
and mseq (Sequence1(a)) pnum = morel a pnum
| mseq (Sequence2(a,b)) pnum
= (morel a pnum) andalso (mseq b pnum)
and morel (Orelement1(a)) pnum = mgel a pnum
| morel (Orelement2(a,b)) pnum
= (mgel a pnum) andalso (morel b pnum)
and mgel (Gelement1(a)) pnum = mstel a pnum
| mgel (Gelement2(a)) pnum = srepl a pnum
| mgel (Gelement4(a,b)) pnum
= (rrepl a pnum) andalso (mgel b pnum)
| mgel (Gelement5(a,b)) pnum
= (mstel a pnum) andalso (mgelL b pnum)
| mgel (Gelement5_1(a,b)) pnum
= (srepl a pnum) andalso (mgelL b pnum)
| mgel (Gelement5_2(a,b)) pnum = (mgelL b pnum)
| mgel other pnum = true
and mgelL (GelementL1(a)) pnum = lrepl a pnum
| mgelL (GelementL2(a,b)) pnum
= (lrepl a pnum) andalso (mgelL b pnum)
and srepl (Sreplicator1(a,b)) pnum
= (ran a pnum) andalso (conc b pnum)
| srepl (Sreplicator2(a,b)) pnum
= (ran a pnum) andalso (imbr b pnum)
and conc (Concseq(a,b)) pnum = mseq a pnum
and imbr (Imbrseq1(a,b,c,d,e)) pnum
= (mseq a pnum) andalso (mseq e pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) pnum
= (mseq a pnum) andalso (mseq d pnum) andalso (mseq g pnum)
| imbr (Imbrseq3(a,b)) pnum = mseq b pnum
| imbr (Imbrseq3s(a,b)) pnum = mseq b pnum
| imbr (Imbrseq4(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq4s(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq5(a,b)) pnum = mseq a pnum
| imbr (Imbrseq5s(a,b)) pnum = mseq a pnum
| imbr (Imbrseq6(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq6s(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq7(a)) pnum = mseq a pnum
| imbr (Imbrseq7s(a)) pnum = mseq a pnum
| imbr (Imbrseq8(a)) pnum = imbr a pnum
| imbr (Imbrseq8s(a)) pnum = imbr a pnum
(*| imbr (Imbrseq9(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq9s(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq10(a,b,c)) = (imbr a) andalso (mseq c)
| imbr (Imbrseq10s(a,b,c)) = (imbr a) andalso (mseq c)
| imbr (Imbrseq11(a,b,c,d,e))
= (mseq a) andalso (imbr c) andalso (mseq e)
| imbr (Imbrseq11s(a,b,c,d,e))
= (mseq a) andalso (imbr c) andalso (mseq e)
| imbr (Imbrseq12(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq13(a,b,c)) = (imbr a) andalso (mseq c)*)
and rrepl (Rreplicator1(a,b,c)) pnum
= (ran a pnum) andalso (conc b pnum)
| rrepl (Rreplicator2(a,b,c)) pnum
= (ran a pnum) andalso (imbr b pnum)
and lrepl (Lreplicator1(a,b,c)) pnum
= (ran a pnum) andalso (conc c pnum)
| lrepl (Lreplicator2(a,b,c)) pnum
= (ran a pnum) andalso (imbr c pnum)
and mstel (Nostar(a)) pnum = mel a pnum
| mstel (Star(a)) pnum = mel a pnum
and mel (Group(a)) pnum = mseq a pnum
| mel other pnum = true
and ran (Range_spec(a,b,c,d)) pnum =
if (iex d) = 0
then (error ("P"^stringofint(pnum)^": 'inc' is equal to zero !!!")
handle Error => (err_cnt:=(!err_cnt)+1; true))
else true
and ran1 (Range_spec(a,b,c,d)) cnum =
if (iex d) = 0
then (error ("C"^stringofint(cnum)^": 'inc' is equal to zero !!!")
handle Error => (err_cnt:=(!err_cnt)+1; true))
else true
in
fun rrest11 x = rres11 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Rrest1.2.
Rrest1.2: For every concatenator and bodyreplicator if in, fi,
inc are integers then (fi - in) div inc + 1 > 0. *)
local
open CSY
open CSR_PRLD
open PRLD
fun rres12 (Program(a)) = mpbody a 1
and mpbody (Programbody1(a)) pnum = mpa a pnum
| mpbody (Programbody2(a)) pnum = mpr a pnum
| mpbody (Programbody3(a)) pnum = brep a pnum
| mpbody (Programbody4(a,b)) pnum = mpbody b pnum
| mpbody (Programbody5(a,b)) pnum
= (mpa a pnum) andalso (mpbody b (pnum+1))
| mpbody (Programbody6(a,b)) pnum
= (mpr a pnum) andalso (mpbody b (pnum+1))
| mpbody (Programbody7(a,b)) pnum
= (brep a pnum) andalso (mpbody b (pnum+1))
and mpa (Path(a)) pnum = mseq a pnum
and mpr (Process(a)) pnum = mseq a pnum
and brep (Bodyreplicator(a,b)) pnum
= (ran a pnum) andalso (bbrep b pnum)
and bbrep (BBodyreplicator1(a)) pnum = mpa a pnum
| bbrep (BBodyreplicator2(a)) pnum = mpr a pnum
| bbrep (BBodyreplicator3(a)) pnum = brep a pnum
| bbrep (BBodyreplicator4(a,b)) pnum
= (mpa a pnum) andalso (bbrep b pnum)
| bbrep (BBodyreplicator5(a,b)) pnum
= (mpr a pnum) andalso (bbrep b pnum)
| bbrep (BBodyreplicator6(a,b)) pnum
= (brep a pnum) andalso (bbrep b pnum)
and mseq (Sequence1(a)) pnum = morel a pnum
| mseq (Sequence2(a,b)) pnum
= (morel a pnum) andalso (mseq b pnum)
and morel (Orelement1(a)) pnum = mgel a pnum
| morel (Orelement2(a,b)) pnum
= (mgel a pnum) andalso (morel b pnum)
and mgel (Gelement1(a)) pnum = mstel a pnum
| mgel (Gelement2(a)) pnum = srep a pnum
| mgel (Gelement4(a,b)) pnum
= (rrepl a pnum) andalso (mgel b pnum)
| mgel (Gelement5(a,b)) pnum
= (mstel a pnum) andalso (mgelL b pnum)
| mgel (Gelement5_1(a,b)) pnum
= (srep a pnum) andalso (mgelL b pnum)
| mgel (Gelement5_2(a,b)) pnum = (mgelL b pnum)
| mgel other pnum = true
and mgelL (GelementL1(a)) pnum = lrepl a pnum
| mgelL (GelementL2(a,b)) pnum
= (lrepl a pnum) andalso (mgelL b pnum)
and srep (Sreplicator1(a,b)) pnum
= (ran a pnum) andalso (conc b pnum)
| srep (Sreplicator2(a,b)) pnum = imbr b pnum
and conc (Concseq(a,b)) pnum = mseq a pnum
and imbr (Imbrseq1(a,b,c,d,e)) pnum
= (mseq a pnum) andalso (mseq e pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) pnum
= (mseq a pnum) andalso (mseq d pnum) andalso (mseq g pnum)
| imbr (Imbrseq3(a,b)) pnum = mseq b pnum
| imbr (Imbrseq3s(a,b)) pnum = mseq b pnum
| imbr (Imbrseq4(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq4s(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq5(a,b)) pnum = mseq a pnum
| imbr (Imbrseq5s(a,b)) pnum = mseq a pnum
| imbr (Imbrseq6(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq6s(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq7(a)) pnum = mseq a pnum
| imbr (Imbrseq7s(a)) pnum = mseq a pnum
| imbr (Imbrseq8(a)) pnum = imbr a pnum
| imbr (Imbrseq8s(a)) pnum = imbr a pnum
(*| imbr (Imbrseq9(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq9s(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq10(a,b,c)) = (imbr a) andalso (mseq c)
| imbr (Imbrseq10s(a,b,c)) = (imbr a) andalso (mseq c)
| imbr (Imbrseq11(a,b,c,d,e))
= (mseq a) andalso (imbr c) andalso (mseq e)
| imbr (Imbrseq11s(a,b,c,d,e))
= (mseq a) andalso (imbr c) andalso (mseq e)
| imbr (Imbrseq12(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq13(a,b,c)) = (imbr a) andalso (mseq c)*)
and rrepl (Rreplicator1(a,b,c)) pnum
= (ran a pnum) andalso (conc b pnum)
| rrepl (Rreplicator2(a,b,c)) pnum = imbr b pnum
and lrepl (Lreplicator1(a,b,c)) pnum
= (ran a pnum) andalso (conc c pnum)
| lrepl (Lreplicator2(a,b,c)) pnum = imbr c pnum
and mstel (Nostar(a)) pnum = mel a pnum
| mstel (Star(a)) pnum = mel a pnum
and mel (Group(a)) pnum = mseq a pnum
| mel other pnum = true
and ran (Range_spec(a,b,c,d)) pnum =
if (iex d) = 0 then true (* false *)
else if ((iex c) - (iex b)) div (iex d) + 1 <= 0
then (error ("P"^stringofint(pnum)^": (fi-ini) div inc+1 <= 0")
handle Error => (err_cnt:=(!err_cnt)+1; true))
else true
in
fun rrest12 x = rres12 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Rrest1.3.
Rrest1.3: For every imbricator, if in, fi, inc are integers then
(fi - in) div inc + 1 <= 0 ===> FSTRIP(LSTRIP(t)) = . *)
local
open CSY
open CSR_PRLD
open PRLD
fun rres13 (Program(a)) = mpbody a 1
and mpbody (Programbody1(a)) pnum = mpa a pnum
| mpbody (Programbody2(a)) pnum = mpr a pnum
| mpbody (Programbody3(a)) pnum = brep a pnum
| mpbody (Programbody4(a,b)) pnum = mpbody b pnum
| mpbody (Programbody5(a,b)) pnum
= (mpa a pnum) andalso (mpbody b (pnum+1))
| mpbody (Programbody6(a,b)) pnum
= (mpr a pnum) andalso (mpbody b (pnum+1))
| mpbody (Programbody7(a,b)) pnum
= (brep a pnum) andalso (mpbody b (pnum+1))
and mpa (Path(a)) pnum = mseq a pnum
and mpr (Process(a)) pnum = mseq a pnum
and brep (Bodyreplicator(a,b)) pnum = bbrep b pnum
and bbrep (BBodyreplicator1(a)) pnum = mpa a pnum
| bbrep (BBodyreplicator2(a)) pnum = mpr a pnum
| bbrep (BBodyreplicator3(a)) pnum = brep a pnum
| bbrep (BBodyreplicator4(a,b)) pnum
= (mpa a pnum) andalso (bbrep b pnum)
| bbrep (BBodyreplicator5(a,b)) pnum
= (mpr a pnum) andalso (bbrep b pnum)
| bbrep (BBodyreplicator6(a,b)) pnum
= (brep a pnum) andalso (bbrep b pnum)
and mseq (Sequence1(a)) pnum = morel a pnum
| mseq (Sequence2(a,b)) pnum
= (morel a pnum) andalso (mseq b pnum)
and morel (Orelement1(a)) pnum = mgel a pnum
| morel (Orelement2(a,b)) pnum
= (mgel a pnum) andalso (morel b pnum)
and mgel (Gelement1(a)) pnum = mstel a pnum
| mgel (Gelement2(a)) pnum = srep a pnum
| mgel (Gelement4(a,b)) pnum
= (rrepl a pnum) andalso (mgel b pnum)
| mgel (Gelement5(a,b)) pnum
= (mstel a pnum) andalso (mgelL b pnum)
| mgel (Gelement5_1(a,b)) pnum
= (srep a pnum) andalso (mgelL b pnum)
| mgel (Gelement5_2(a,b)) pnum = (mgelL b pnum)
| mgel other pnum = true
and mgelL (GelementL1(a)) pnum = lrepl a pnum
| mgelL (GelementL2(a,b)) pnum
= (lrepl a pnum) andalso (mgelL b pnum)
and srep (Sreplicator1(a,b)) pnum = conc b pnum
| srep (Sreplicator2(a,b)) pnum
= ((ran a pnum) orelse (imb b pnum)) andalso (imbr b pnum)
and conc (Concseq(a,b)) pnum = mseq a pnum
and imbr (Imbrseq1(a,b,c,d,e)) pnum
= (mseq a pnum) andalso (mseq e pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) pnum
= (mseq a pnum) andalso (mseq d pnum) andalso (mseq g pnum)
| imbr (Imbrseq3(a,b)) pnum = mseq b pnum
| imbr (Imbrseq3s(a,b)) pnum = mseq b pnum
| imbr (Imbrseq4(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq4s(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq5(a,b)) pnum = mseq a pnum
| imbr (Imbrseq5s(a,b)) pnum = mseq a pnum
| imbr (Imbrseq6(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq6s(a,b,c,d)) pnum
= (mseq a pnum) andalso (mseq d pnum)
| imbr (Imbrseq7(a)) pnum = mseq a pnum
| imbr (Imbrseq7s(a)) pnum = mseq a pnum
| imbr (Imbrseq8(a)) pnum = imbr a pnum
| imbr (Imbrseq8s(a)) pnum = imbr a pnum
(*| imbr (Imbrseq9(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq9s(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq10(a,b,c)) = (imbr a) andalso (mseq c)
| imbr (Imbrseq10s(a,b,c)) = (imbr a) andalso (mseq c)
| imbr (Imbrseq11(a,b,c,d,e))
= (mseq a) andalso (imbr c) andalso (mseq e)
| imbr (Imbrseq11s(a,b,c,d,e))
= (mseq a) andalso (imbr c) andalso (mseq e)
| imbr (Imbrseq12(a,b,c)) = (mseq a) andalso (imbr c)
| imbr (Imbrseq13(a,b,c)) = (imbr a) andalso (mseq c)*)
and rrepl (Rreplicator1(a,b,c)) pnum = conc b pnum
| rrepl (Rreplicator2(a,b,c)) pnum
= ((ran a pnum) orelse (imb b pnum)) andalso (imbr b pnum)
and lrepl (Lreplicator1(a,b,c)) pnum = conc c pnum
| lrepl (Lreplicator2(a,b,c)) pnum
= ((ran a pnum) orelse (imb c pnum)) andalso (imbr c pnum)
and mstel (Nostar(a)) pnum = mel a pnum
| mstel (Star(a)) pnum = mel a pnum
and mel (Group(a)) pnum = mseq a pnum
| mel other pnum = true
and ran (Range_spec(a,b,c,d)) pnum =
if ((iex c) - (iex b)) div (iex d) + 1 <= 0
then false
else true
and imb (Imbrseq2(a,b,c,d,e,f,g)) pnum = true
| imb (Imbrseq3(a,b)) pnum = true
| imb (Imbrseq3s(a,b)) pnum = true
| imb (Imbrseq4(a,b,c,d)) pnum = true
| imb (Imbrseq4s(a,b,c,d)) pnum = true
| imb (Imbrseq5(a,b)) pnum = true
| imb (Imbrseq5s(a,b)) pnum = true
| imb (Imbrseq6(a,b,c,d)) pnum = true
| imb (Imbrseq6s(a,b,c,d)) pnum = true
| imb (Imbrseq7(a)) pnum = true
| imb (Imbrseq7s(a)) pnum = true
| imb (Imbrseq8(a)) pnum = true
| imb (Imbrseq8s(a)) pnum = true
(*| imb (Imbrseq9(a,b,c)) = true
| imb (Imbrseq9s(a,b,c)) = true
| imb (Imbrseq10(a,b,c)) = true
| imb (Imbrseq10s(a,b,c)) = true
| imb (Imbrseq11(a,b,c,d,e)) = true
| imb (Imbrseq11s(a,b,c,d,e)) = true
| imb (Imbrseq12(a,b,c)) = true
| imb (Imbrseq13(a,b,c)) = true*)
| imb (Imbrseq1(a,b,c,d,e)) pnum
= (error ("P"^stringofint(pnum)^
": (fi - in) div inc + 1 <= 0 and FSTRIP(LSTRIP(t)) = null")
handle Error => (err_cnt := (!err_cnt) + 1; true))
in
fun rrest13 x = rres13 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Rrest2.
Rrest2: The replicators should generate indexed events permitted
by the corresponding collectivisors. *)
local
open CSY
open CSR_PRLD
open PRLD
type temp = {n1 : string,
lower : int,
upper : int,
step : int};
fun rres2 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum []
| mpbody (Programbody2(a)) tbl pnum = mpr a tbl pnum []
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum []
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum []) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum []) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum []) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum l = mseq a tbl pnum l
and mpr (Process(a)) tbl pnum l = mseq a tbl pnum l
and brep (Bodyreplicator(a,b)) tbl pnum l
= bbrep b tbl pnum ((ran a) @ l)
and bbrep (BBodyreplicator1(a)) tbl pnum l = mpa a tbl pnum l
| bbrep (BBodyreplicator2(a)) tbl pnum l = mpr a tbl pnum l
| bbrep (BBodyreplicator3(a)) tbl pnum l = brep a tbl pnum l
| bbrep (BBodyreplicator4(a,b)) tbl pnum l
= (mpa a tbl pnum l) andalso (bbrep b tbl pnum l)
| bbrep (BBodyreplicator5(a,b)) tbl pnum l
= (mpr a tbl pnum l) andalso (bbrep b tbl pnum l)
| bbrep (BBodyreplicator6(a,b)) tbl pnum l
= (brep a tbl pnum l) andalso (bbrep b tbl pnum l)
and mseq (Sequence1(a)) tbl pnum l = morel a tbl pnum l
| mseq (Sequence2(a,b)) tbl pnum l
= (morel a tbl pnum l) andalso (mseq b tbl pnum l)
and morel (Orelement1(a)) tbl pnum l = mgel a tbl pnum l
| morel (Orelement2(a,b)) tbl pnum l
= (mgel a tbl pnum l) andalso (morel b tbl pnum l)
and mgel (Gelement1(a)) tbl pnum l = mstel a tbl pnum l
| mgel (Gelement2(a)) tbl pnum l = srepl a tbl pnum l
| mgel (Gelement4(a,b)) tbl pnum l
= (rrepl a tbl pnum l) andalso (mgel b tbl pnum l)
| mgel (Gelement5(a,b)) tbl pnum l
= (mstel a tbl pnum l) andalso (mgelL b tbl pnum l)
| mgel (Gelement5_1(a,b)) tbl pnum l
= (srepl a tbl pnum l) andalso (mgelL b tbl pnum l)
| mgel (Gelement5_2(a,b)) tbl pnum l = (mgelL b tbl pnum l)
| mgel other tbl pnum l = true
and mgelL (GelementL1(a)) tbl pnum l = lrepl a tbl pnum l
| mgelL (GelementL2(a,b)) tbl pnum l
= (lrepl a tbl pnum l) andalso (mgelL b tbl pnum l)
and srepl (Sreplicator1(a,b)) tbl pnum l
= conc b tbl pnum ((ran a) @ l)
| srepl (Sreplicator2(a,b)) tbl pnum l
= imbr b tbl pnum ((ran a) @ l)
and conc (Concseq(a,b)) tbl pnum l = mseq a tbl pnum l
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum l
= (mseq a tbl pnum l) andalso (mseq e tbl pnum l)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum l
= (mseq a tbl pnum l) andalso (mseq d tbl pnum l)
andalso (mseq g tbl pnum l)
| imbr (Imbrseq3(a,b)) tbl pnum l = mseq b tbl pnum l
| imbr (Imbrseq3s(a,b)) tbl pnum l = mseq b tbl pnum l
| imbr (Imbrseq4(a,b,c,d)) tbl pnum l
= (mseq a tbl pnum l) andalso (mseq d tbl pnum l)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum l
= (mseq a tbl pnum l) andalso (mseq d tbl pnum l)
| imbr (Imbrseq5(a,b)) tbl pnum l = mseq a tbl pnum l
| imbr (Imbrseq5s(a,b)) tbl pnum l = mseq a tbl pnum l
| imbr (Imbrseq6(a,b,c,d)) tbl pnum l
= (mseq a tbl pnum l) andalso (mseq d tbl pnum l)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum l
= (mseq a tbl pnum l) andalso (mseq d tbl pnum l)
| imbr (Imbrseq7(a)) tbl pnum l = mseq a tbl pnum l
| imbr (Imbrseq7s(a)) tbl pnum l = mseq a tbl pnum l
| imbr (Imbrseq8(a)) tbl pnum l = imbr a tbl pnum l
| imbr (Imbrseq8s(a)) tbl pnum l = imbr a tbl pnum l
(*| imbr (Imbrseq9(a,b,c)) tbl l
= (mseq a tbl l) andalso (imbr c tbl l)
| imbr (Imbrseq9s(a,b,c)) tbl l
= (mseq a tbl l) andalso (imbr c tbl l)
| imbr (Imbrseq10(a,b,c)) tbl l
= (imbr a tbl l) andalso (mseq c tbl l)
| imbr (Imbrseq10s(a,b,c))tbl l
= (imbr a tbl l) andalso (mseq c tbl l)
| imbr (Imbrseq11(a,b,c,d,e)) tbl l
= (mseq a tbl l) andalso (imbr c tbl l)
andalso (mseq e tbl l)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl l
= (mseq a tbl l) andalso (imbr c tbl l)
andalso (mseq e tbl l)
| imbr (Imbrseq12(a,b,c)) tbl l
= (mseq a tbl l) andalso (imbr c tbl l)
| imbr (Imbrseq13(a,b,c)) tbl l
= (imbr a tbl l) andalso (mseq c tbl l)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum l
= conc b tbl pnum ((ran a) @ l)
| rrepl (Rreplicator2(a,b,c)) tbl pnum l
= imbr b tbl pnum ((ran a) @ l)
and lrepl (Lreplicator1(a,b,c)) tbl pnum l
= conc c tbl pnum ((ran a) @ l)
| lrepl (Lreplicator2(a,b,c)) tbl pnum l
= imbr c tbl pnum ((ran a) @ l)
and mstel (Nostar(a)) tbl pnum l = mel a tbl pnum l
| mstel (Star(a)) tbl pnum l = mel a tbl pnum l
and mel (Group(a)) tbl pnum l = mseq a tbl pnum l
| mel (Element(a)) tbl pnum l = mev a tbl pnum l
and mev (Event3(a,b)) tbl pnum l = mevb b (na a) tbl pnum l 1
| mev other tbl pnum l = true
and mevb (Meventbody1(a)) str tbl pnum l pos
= if isarray(str,tbl)
then check a str tbl pnum l pos else true (*false*)
| mevb (Meventbody3(a,b)) str tbl pnum l pos
= if isarray(str,tbl) then (check a str tbl pnum l pos)
andalso mevb b str tbl pnum l (pos+1)
else true (*false*)
| mevb other str tbl pnum l pos = true
and na (Name(a)) = a
(* function "ran" create a list of index range *)
and ran (Range_spec(a,b,c,d))
= [{n1=ivar a, lower=iex b, upper=iex c, step=iex d}]
and check (Iexpr2(Rangevariable(Name a))) str tbl pnum l pos
= if mem1 (range1 str tbl pos) (range2 a l) then true
else (error ("P"^stringofint(pnum)^
": Range is out of boundary")
handle Error => (err_cnt := (!err_cnt) + 1; true))
| check other str tbl pnum l pos = true
(* function "range1", "mkrange1" and "mkrange11" create a list of
the index value *)
and range1 str ((h:Arraytable)::x) pos
= if str = (#name h)
then mkrange1 (#value h) pos
else range1 str x pos
| range1 str [] pos = []
and mkrange1 ((b:bound)::x) pos
= if pos = (#pos b)
then mkrange11 (#lower b) (#upper b) (#step b)
else mkrange1 x pos
| mkrange1 [] pos = []
and mkrange11 ini fi inc = if ini <= fi andalso inc > 0
then [ini] @ mkrange11 (ini+inc) fi inc
else if ini >= fi andalso inc < 0
then [ini] @ mkrange11(ini+inc) fi inc
else []
and range2 a ((h:temp)::x)
= if a = (#n1 h)
then mkrange11 (#lower h) (#upper h) (#step h)
else range2 a x
| range2 a [] = []
and ivar (Indexvariable(Name a)) = a
and mem1 x (y::z) = if member x y then mem1 x z else false
| mem1 x [] = true
and isarray(str,(h:Arraytable)::x)
= if str = (#name h) then true else isarray(str,x)
| isarray (str,[]) = false
in
fun rrest2 x = rres2 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Drest1.
Drest1: For every distributor sep dim range[msequence], msequence
must contain at least one slice event. *)
(*Note: all names of functions with "1" are involved in distributor*)
local
open CSY
open CSR_PRLD
open PRLD
fun dres1 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum
| mpbody (Programbody2(a)) tbl pnum = mpr a tbl pnum
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum = mseq a tbl pnum
and mpr (Process(a)) tbl pnum = mseq a tbl pnum
and brep (Bodyreplicator(a,b)) tbl pnum = bbrep b tbl pnum
and bbrep (BBodyreplicator1(a)) tbl pnum = mpa a tbl pnum
| bbrep (BBodyreplicator2(a)) tbl pnum = mpr a tbl pnum
| bbrep (BBodyreplicator3(a)) tbl pnum = brep a tbl pnum
| bbrep (BBodyreplicator4(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator5(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator6(a,b)) tbl pnum
= (brep a tbl pnum) andalso (bbrep b tbl pnum)
and mseq (Sequence1(a)) tbl pnum = morel a tbl pnum
| mseq (Sequence2(a,b)) tbl pnum
= (morel a tbl pnum) orelse (mseq b tbl pnum)
and morel (Orelement1(a)) tbl pnum = mgel a tbl pnum
| morel (Orelement2(a,b)) tbl pnum
= (mgel a tbl pnum) orelse (morel b tbl pnum)
and mgel (Gelement1(a)) tbl pnum = mstel a tbl pnum
| mgel (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel (Gelement3(a)) tbl pnum = check((dist a tbl pnum),pnum)
| mgel (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel b tbl pnum)
| mgel (Gelement5(a,b)) tbl pnum
= (mstel a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_2(a,b)) tbl pnum
= (check((dist a tbl pnum),pnum)) andalso (mgelL b tbl pnum)
and mgelL (GelementL1(a)) tbl pnum = lrepl a tbl pnum
| mgelL (GelementL2(a,b)) tbl pnum
= (lrepl a tbl pnum) andalso (mgelL b tbl pnum)
and srepl (Sreplicator1(a,b)) tbl pnum = conc b tbl pnum
| srepl (Sreplicator2(a,b)) tbl pnum = imbr b tbl pnum
and conc (Concseq(a,b)) tbl pnum = mseq a tbl pnum
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum
= (mseq a tbl pnum) andalso (mseq e tbl pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
andalso (mseq g tbl pnum)
| imbr (Imbrseq3(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq3s(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq4(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq5(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq5s(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq6(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq7(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq7s(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq8(a)) tbl pnum = imbr a tbl pnum
| imbr (Imbrseq8s(a)) tbl pnum = imbr a tbl pnum
(*| imbr (Imbrseq9(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum = conc b tbl pnum
| rrepl (Rreplicator2(a,b,c)) tbl pnum = imbr b tbl pnum
and lrepl (Lreplicator1(a,b,c)) tbl pnum = conc c tbl pnum
| lrepl (Lreplicator2(a,b,c)) tbl pnum = imbr c tbl pnum
and dist (Distributor1(a,b,c,d)) tbl pnum = mseq1 d tbl pnum
| dist (Distributor2(a,b,c)) tbl pnum = mseq1 c tbl pnum
| dist (Distributor3(a,b,c)) tbl pnum = mseq1 c tbl pnum
| dist (Distributor4(a,b)) tbl pnum = mseq1 b tbl pnum
and mseq1 (Sequence1(a)) tbl pnum = morel1 a tbl pnum
| mseq1 (Sequence2(a,b)) tbl pnum
= (morel1 a tbl pnum) orelse (mseq1 b tbl pnum)
and morel1 (Orelement1(a)) tbl pnum = mgel1 a tbl pnum
| morel1 (Orelement2(a,b)) tbl pnum
= (mgel1 a tbl pnum) orelse (morel1 b tbl pnum)
and mgel1 (Gelement1(a)) tbl pnum = mstel1 a tbl pnum
| mgel1 (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel1 (Gelement3(a)) tbl pnum = dist a tbl pnum
| mgel1 (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel1 b tbl pnum)
| mgel1 (Gelement5(a,b)) tbl pnum
= (mstel1 a tbl pnum) andalso (mgelL b tbl pnum)
| mgel1 (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel1 (Gelement5_2(a,b)) tbl pnum
= (dist a tbl pnum) andalso (mgelL b tbl pnum)
and mstel1 (Nostar(a)) tbl pnum = mel1 a tbl pnum
| mstel1 (Star(a)) tbl pnum = mel1 a tbl pnum
and mel1 (Element(a)) tbl pnum = ev a tbl
| mel1 (Group(a)) tbl pnum = mseq1 a tbl pnum
and mstel (Nostar(a)) tbl pnum = mel a tbl pnum
| mstel (Star(a)) tbl pnum = mel a tbl pnum
and mel (Element(a)) tbl pnum = true
| mel (Group(a)) tbl pnum = mseq a tbl pnum
and ev (Event1(Name a)) tbl
= if mem (tbl,a) then true else false
| ev (Event2(Name a)) tbl
= if mem (tbl,a) then true else false
| ev (Event3(Name a,b)) tbl
= if mem (tbl,a) then (mevbody b) else false
and mevbody (Empty) = true
| mevbody (Meventbody1(a)) = false
| mevbody (Meventbody2(a)) = true
| mevbody (Meventbody3(a,b)) = mevbody b
| mevbody (Meventbody4(a)) = true
and check(tf,pnum) = if tf then true
else (error ("P"^stringofint(pnum)
^": No slice event exist in distributor")
handle Error => (err_cnt := (!err_cnt) + 1; true))
in
fun drest1 x = dres1 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Drest2.1.
Drest2.1: If both range and dim are blank then then number of
sections generated by the rightmost distributable
(current) dimension must be the same for all slice
events occurring in msequence *)
local
open CSY
open CSR_PRLD
open PRLD
type posl = {p : int, d : int}
type temp1 = {name : string, dim : int list, pos : posl list}
fun dres21 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum
| mpbody (Programbody2(a)) tbl pnum = mpr a tbl pnum
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum = mseq a tbl pnum
and mpr (Process(a)) tbl pnum = mseq a tbl pnum
and brep (Bodyreplicator(a,b)) tbl pnum = bbrep b tbl pnum
and bbrep (BBodyreplicator1(a)) tbl pnum = mpa a tbl pnum
| bbrep (BBodyreplicator2(a)) tbl pnum = mpr a tbl pnum
| bbrep (BBodyreplicator3(a)) tbl pnum = brep a tbl pnum
| bbrep (BBodyreplicator4(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator5(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator6(a,b)) tbl pnum
= (brep a tbl pnum) andalso (bbrep b tbl pnum)
and mseq (Sequence1(a)) tbl pnum = morel a tbl pnum
| mseq (Sequence2(a,b)) tbl pnum
= (morel a tbl pnum) orelse (mseq b tbl pnum)
and morel (Orelement1(a)) tbl pnum = mgel a tbl pnum
| morel (Orelement2(a,b)) tbl pnum
= (mgel a tbl pnum) orelse (morel b tbl pnum)
and mgel (Gelement1(a)) tbl pnum = mstel a tbl pnum
| mgel (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel (Gelement3(a)) tbl pnum
= check ((dist a tbl pnum [] 0),tbl,pnum)
| mgel (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel b tbl pnum)
| mgel (Gelement5(a,b)) tbl pnum
= (mstel a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_2(a,b)) tbl pnum
= (check((dist a tbl pnum [] 0),tbl,pnum))
andalso (mgelL b tbl pnum)
and mgelL (GelementL1(a)) tbl pnum = lrepl a tbl pnum
| mgelL (GelementL2(a,b)) tbl pnum
= (lrepl a tbl pnum) andalso (mgelL b tbl pnum)
and dist (Distributor1(a,b,c,d)) tbl pnum l ct1
= mseq1 d tbl pnum (l @ [{p=ct1+1, d=iex1 b}]) (ct1+1)
| dist (Distributor2(a,b,c)) tbl pnum l ct1
= mseq1 c tbl pnum (l @ [{p=ct1+1, d=iex1 b}]) (ct1+1)
| dist (Distributor3(a,b,c)) tbl pnum l ct1
= mseq1 c tbl pnum (l @ [{p=ct1+1, d=(~1)}]) (ct1+1)
| dist (Distributor4(a,b)) tbl pnum l ct1
= mseq1 b tbl pnum (l @ [{p=ct1+1,d=0}]) (ct1+1)
and mstel (Nostar(a)) tbl pnum = mel a tbl pnum
| mstel (Star(a)) tbl pnum = mel a tbl pnum
and mel (Element(a)) tbl pnum = true
| mel (Group(a)) tbl pnum = mseq a tbl pnum
and srepl (Sreplicator1(a,b)) tbl pnum = conc b tbl pnum
| srepl (Sreplicator2(a,b)) tbl pnum = imbr b tbl pnum
and conc (Concseq(a,b)) tbl pnum = mseq a tbl pnum
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum
= (mseq a tbl pnum) andalso (mseq e tbl pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
andalso (mseq g tbl pnum)
| imbr (Imbrseq3(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq3s(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq4(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq5(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq5s(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq6(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq7(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq7s(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq8(a)) tbl pnum = imbr a tbl pnum
| imbr (Imbrseq8s(a)) tbl pnum = imbr a tbl pnum
(*| imbr (Imbrseq9(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum = conc b tbl pnum
| rrepl (Rreplicator2(a,b,c)) tbl pnum = imbr b tbl pnum
and lrepl (Lreplicator1(a,b,c)) tbl pnum = conc c tbl pnum
| lrepl (Lreplicator2(a,b,c)) tbl pnum = imbr c tbl pnum
and mseq1 (Sequence1(a)) tbl pnum l ct1
= morel1 a tbl pnum l ct1
| mseq1 (Sequence2(a,b)) tbl pnum l ct1
= (morel1 a tbl pnum l ct1) @ (mseq1 b tbl pnum l ct1)
and morel1 (Orelement1(a)) tbl pnum l ct1
= mgel1 a tbl pnum l ct1
| morel1 (Orelement2(a,b)) tbl pnum l ct1
= (mgel1 a tbl pnum l ct1) @ (morel1 b tbl pnum l ct1)
and mgel1 (Gelement1(a)) tbl pnum l ct1 = mstel1 a tbl pnum l ct1
| mgel1 (Gelement2(a)) tbl pnum l ct1 = srepl1 a tbl pnum l ct1
| mgel1 (Gelement3(a)) tbl pnum l ct1 = dist a tbl pnum l ct1
| mgel1 (Gelement4(a,b)) tbl pnum l ct1
= (rrepl1 a tbl pnum l ct1) @ (mgel1 b tbl pnum l ct1)
| mgel1 (Gelement5(a,b)) tbl pnum l ct1
= (mstel1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
| mgel1 (Gelement5_1(a,b)) tbl pnum l ct1
= (srepl1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
| mgel1 (Gelement5_2(a,b)) tbl pnum l ct1
= (dist a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
and mgelL1 (GelementL1(a)) tbl pnum l ct1 = lrepl1 a tbl pnum l ct1
| mgelL1 (GelementL2(a,b)) tbl pnum l ct1
= (lrepl1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
and mstel1 (Nostar(a)) tbl pnum l ct1 = mel1 a tbl pnum l ct1
| mstel1 (Star(a)) tbl pnum l ct1 = mel1 a tbl pnum l ct1
and mel1 (Element(a)) tbl pnum l ct1 = ev a tbl l ct1
| mel1 (Group(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
and srepl1 (Sreplicator1(a,b)) tbl pnum l ct1
= conc1 b tbl pnum l ct1
| srepl1 (Sreplicator2(a,b)) tbl pnum l ct1
= imbr1 b tbl pnum l ct1
and conc1 (Concseq(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
and imbr1 (Imbrseq1(a,b,c,d,e)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 e tbl pnum l ct1)
| imbr1 (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1) @
(mseq1 g tbl pnum l ct1)
| imbr1 (Imbrseq3(a,b)) tbl pnum l ct1 = mseq1 b tbl pnum l ct1
| imbr1 (Imbrseq3s(a,b)) tbl pnum l ct1 = mseq1 b tbl pnum l ct1
| imbr1 (Imbrseq4(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq4s(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq5(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq5s(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq6(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq6s(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq7(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq7s(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq8(a)) tbl pnum l ct1 = imbr1 a tbl pnum l ct1
| imbr1 (Imbrseq8s(a)) tbl pnum l ct1 = imbr1 a tbl pnum l ct1
(*| imbr1 (Imbrseq9(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq9s(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq10(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq10s(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq11(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq11s(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq12(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq13(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)*)
and rrepl1 (Rreplicator1(a,b,c)) tbl pnum l ct1
= conc1 b tbl pnum l ct1
| rrepl1 (Rreplicator2(a,b,c)) tbl pnum l ct1
= imbr1 b tbl pnum l ct1
and lrepl1 (Lreplicator1(a,b,c)) tbl pnum l ct1
= conc1 c tbl pnum l ct1
| lrepl1 (Lreplicator2(a,b,c)) tbl pnum l ct1
= imbr1 c tbl pnum l ct1
and ev (Event1(Name a)) tbl l ct1
= if mem (tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else []
| ev (Event2(Name a)) tbl l ct1
= if mem(tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else [] (* if it is not an array (a simple event) *)
| ev (Event3(Name a,b)) tbl l ct1
= if mem (tbl,a) then [{name=a,dim=(mevbody b 0), pos=l}]
else [] (*error "not an array"
handle Error => (err_cnt := (!err_cnt) + 1; [])*)
and mevbody (Empty) ct = [ct+2] @ [ct+1]
| mevbody (Meventbody1(a)) ct = []
| mevbody (Meventbody2(a)) ct = (mevbody a (ct+1)) @ [ct+1]
| mevbody (Meventbody3(a,b)) ct = mevbody b (ct+1)
| mevbody (Meventbody4(a)) ct = [ct+2]
and getlist(name,((a:Arraytable)::x))
= if name = (#name a) then count1(1,(#dim a))
else getlist(name,x)
| getlist(name,[]) = []
and count1(ini,fi)
= if ini <= fi
then (count1((ini+1),fi)) @ [ini]
else []
and check(l,tbl,pnum)
= if chk (l,tbl) then check1(remv(l),tbl,pnum)
else (error ("P"^stringofint(pnum)
^": Wrong number of empty index-fields")
handle Error => (err_cnt := (!err_cnt) + 1; true))
(* check the case like: has array c(3,3,3) but ;[,[c]] *)
and chk(a::x,tbl) = if mem(tbl,(#name a)) then
(if (length(#dim a) <> length(#pos a)) then false
else chk(x,tbl))
else true
| chk ([],tbl) = true
(* remove those which their range and dim are not blank *)
and remv ((a:temp1)::x)
= if dimlist((#dim a),(#pos a))=[] orelse poslist(#pos a)=[]
then remv x
else [{name=(#name a),
dim=dimlist((#dim a),(#pos a)),
pos=poslist(#pos a)}]
@ remv x
| remv [] = []
and dimlist(dim,pos::x) = if (#d pos) = 0 then dimlist(dim, x)
else dimlist(dimlist1(dim,(#d pos)),x)
| dimlist(dim,[]) = dim
and dimlist1(dim::x,d) = if d = (~1) then dimlist1(x,d)
else if d = dim then dimlist1(x,d)
else [dim] @ dimlist1(x,d)
| dimlist1([],d) = []
and poslist(pos::x) = if (#d pos) = 0 then [pos] @ poslist(x)
else poslist(x)
| poslist([]) = []
and check1(((a:temp1):: x),tbl,pnum)
= check2 (getnum((#name a),(#dim a),tbl)) x tbl pnum
(getp(#pos a)) (newlist((#name a),(#dim a),(#pos a)))
| check1([],tbl,pnum)= true
and check2 num ((a:temp1)::x) tbl pnum p l
= if p<>getp(#pos a) then check2 num x tbl pnum p (l @ [a])
else if num<>getnum((#name a),(#dim a),tbl)
then (error ("P"^stringofint(pnum)
^": Do not have the same number of sections")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else check2 num x tbl pnum p
(l @ (newlist((#name a),(#dim a),(#pos a))))
| check2 num [] tbl pnum p l = check1(l,tbl,pnum)
and getp (a::x) =(#p a)
| getp [] = error "Error" handle Error
=> (err_cnt := (!err_cnt) + 1; 0)
and newlist (name,a::x,b::y)
= if x=[] andalso y=[] then [] else [{name=name,dim=x,pos=y}]
| newlist (name,[],[]) = error "Error"
| newlist (name,l,[]) = error "Error"
| newlist (name,[],l) = error "Error"
and getnum(na,dim,((a:Arraytable)::x))
= if na <> (#name a) then getnum(na,dim,x)
else getnum1(hd(dim),(#value a))
| getnum(na,dim,[]) = 0 (*error (na^" is not an array")
handle Error => (err_cnt := (!err_cnt) + 1; 0) *)
and getnum1(dim,(v:bound)::x)
= if dim <> (#pos v) then getnum1(dim,x)
else count2 ((#lower v),(#upper v),(#step v))
| getnum1(dim,[]) = 0 (*error "do not have that dimension"
handle Error => (err_cnt := (!err_cnt) + 1; 0) *)
and count2(ini,fi,inc)
= if ini <= fi andalso inc > 0
then 1 + count2((ini+inc),fi,inc)
else if ini >= fi andalso inc < 0
then 1 + count2((ini+inc),fi,inc)
else 0
in
fun drest21 x = dres21 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Drest2.2.
Drest2.2: If range is blank, dim = j and j is an integer, then
the number of sections generated by jth dimension must
be the same for all slice events occuring in msequence
and having the jth dimension distributable. *)
local
open CSY
open CSR_PRLD
open PRLD
type posl = {p : int, d : int}
type temp1 = {name : string, dim : int list, pos : posl list}
fun dres22 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum
| mpbody (Programbody2(a)) tbl pnum = mpr a tbl pnum
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum = mseq a tbl pnum
and mpr (Process(a)) tbl pnum = mseq a tbl pnum
and brep (Bodyreplicator(a,b)) tbl pnum = bbrep b tbl pnum
and bbrep (BBodyreplicator1(a)) tbl pnum = mpa a tbl pnum
| bbrep (BBodyreplicator2(a)) tbl pnum = mpr a tbl pnum
| bbrep (BBodyreplicator3(a)) tbl pnum = brep a tbl pnum
| bbrep (BBodyreplicator4(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator5(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator6(a,b)) tbl pnum
= (brep a tbl pnum) andalso (bbrep b tbl pnum)
and mseq (Sequence1(a)) tbl pnum = morel a tbl pnum
| mseq (Sequence2(a,b)) tbl pnum
= (morel a tbl pnum) orelse (mseq b tbl pnum)
and morel (Orelement1(a)) tbl pnum = mgel a tbl pnum
| morel (Orelement2(a,b)) tbl pnum
= (mgel a tbl pnum) orelse (morel b tbl pnum)
and mgel (Gelement1(a)) tbl pnum = mstel a tbl pnum
| mgel (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel (Gelement3(a)) tbl pnum
= check ((dist a tbl pnum [] 0),tbl,pnum)
| mgel (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel b tbl pnum)
| mgel (Gelement5(a,b)) tbl pnum
= (mstel a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_2(a,b)) tbl pnum
= (check((dist a tbl pnum [] 0),tbl,pnum))
andalso (mgelL b tbl pnum)
and mgelL (GelementL1(a)) tbl pnum = lrepl a tbl pnum
| mgelL (GelementL2(a,b)) tbl pnum
= (lrepl a tbl pnum) andalso (mgelL b tbl pnum)
and dist (Distributor1(a,b,c,d)) tbl pnum l ct1
= mseq1 d tbl pnum (l @ [{p=(~1), d=chkdim(b,pnum)}]) (ct1+1)
| dist (Distributor2(a,b,c)) tbl pnum l ct1
= mseq1 c tbl pnum (l @ [{p=ct1+1, d=chkdim(b,pnum)}]) (ct1+1)
| dist (Distributor3(a,b,c)) tbl pnum l ct1
= mseq1 c tbl pnum (l @ [{p=ct1+1, d=0}]) (ct1+1)
| dist (Distributor4(a,b)) tbl pnum l ct1
= mseq1 b tbl pnum (l @ [{p=ct1+1,d=0}]) (ct1+1)
and mstel (Nostar(a)) tbl pnum = mel a tbl pnum
| mstel (Star(a)) tbl pnum = mel a tbl pnum
and mel (Element(a)) tbl pnum = true
| mel (Group(a)) tbl pnum = mseq a tbl pnum
and srepl (Sreplicator1(a,b)) tbl pnum = conc b tbl pnum
| srepl (Sreplicator2(a,b)) tbl pnum = imbr b tbl pnum
and conc (Concseq(a,b)) tbl pnum = mseq a tbl pnum
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum
= (mseq a tbl pnum) andalso (mseq e tbl pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
andalso (mseq g tbl pnum)
| imbr (Imbrseq3(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq3s(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq4(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq5(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq5s(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq6(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq7(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq7s(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq8(a)) tbl pnum = imbr a tbl pnum
| imbr (Imbrseq8s(a)) tbl pnum = imbr a tbl pnum
(*| imbr (Imbrseq9(a,b,c)) tbl pnum
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl = (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl = (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl = (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum = conc b tbl pnum
| rrepl (Rreplicator2(a,b,c)) tbl pnum = imbr b tbl pnum
and lrepl (Lreplicator1(a,b,c)) tbl pnum = conc c tbl pnum
| lrepl (Lreplicator2(a,b,c)) tbl pnum = imbr c tbl pnum
and mseq1 (Sequence1(a)) tbl pnum l ct1 = morel1 a tbl pnum l ct1
| mseq1 (Sequence2(a,b)) tbl pnum l ct1
= (morel1 a tbl pnum l ct1) @ (mseq1 b tbl pnum l ct1)
and morel1 (Orelement1(a)) tbl pnum l ct1 = mgel1 a tbl pnum l ct1
| morel1 (Orelement2(a,b)) tbl pnum l ct1
= (mgel1 a tbl pnum l ct1) @ (morel1 b tbl pnum l ct1)
and mgel1 (Gelement1(a)) tbl pnum l ct1 = mstel1 a tbl pnum l ct1
| mgel1 (Gelement2(a)) tbl pnum l ct1 = srepl1 a tbl pnum l ct1
| mgel1 (Gelement3(a)) tbl pnum l ct1 = dist a tbl pnum l ct1
| mgel1 (Gelement4(a,b)) tbl pnum l ct1
= (rrepl1 a tbl pnum l ct1) @ (mgel1 b tbl pnum l ct1)
| mgel1 (Gelement5(a,b)) tbl pnum l ct1
= (mstel1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
| mgel1 (Gelement5_1(a,b)) tbl pnum l ct1
= (srepl1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
| mgel1 (Gelement5_2(a,b)) tbl pnum l ct1
= (dist a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
and mgelL1 (GelementL1(a)) tbl pnum l ct1 = lrepl1 a tbl pnum l ct1
| mgelL1 (GelementL2(a,b)) tbl pnum l ct1
= (lrepl1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
and mstel1 (Nostar(a)) tbl pnum l ct1 = mel1 a tbl pnum l ct1
| mstel1 (Star(a)) tbl pnum l ct1 = mel1 a tbl pnum l ct1
and mel1 (Element(a)) tbl pnum l ct1 = ev a tbl pnum l ct1
| mel1 (Group(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
and srepl1 (Sreplicator1(a,b)) tbl pnum l ct1
= conc1 b tbl pnum l ct1
| srepl1 (Sreplicator2(a,b)) tbl pnum l ct1
= imbr1 b tbl pnum l ct1
and conc1 (Concseq(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
and imbr1 (Imbrseq1(a,b,c,d,e)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 e tbl pnum l ct1)
| imbr1 (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1) @
(mseq1 g tbl pnum l ct1)
| imbr1 (Imbrseq3(a,b)) tbl pnum l ct1 = mseq1 b tbl pnum l ct1
| imbr1 (Imbrseq3s(a,b)) tbl pnum l ct1 = mseq1 b tbl pnum l ct1
| imbr1 (Imbrseq4(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq4s(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq5(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq5s(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq6(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq6s(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq7(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq7s(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq8(a)) tbl pnum l ct1 = imbr1 a tbl pnum l ct1
| imbr1 (Imbrseq8s(a)) tbl pnum l ct1 = imbr1 a tbl pnum l ct1
(*| imbr1 (Imbrseq9(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq9s(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq10(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq10s(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq11(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq11s(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq12(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq13(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)*)
and rrepl1 (Rreplicator1(a,b,c)) tbl pnum l ct1
= conc1 b tbl pnum l ct1
| rrepl1 (Rreplicator2(a,b,c)) tbl pnum l ct1
= imbr1 b tbl pnum l ct1
and lrepl1 (Lreplicator1(a,b,c)) tbl pnum l ct1
= conc1 c tbl pnum l ct1
| lrepl1 (Lreplicator2(a,b,c)) tbl pnum l ct1
= imbr1 c tbl pnum l ct1
and ev (Event1(Name a)) tbl pnum l ct1
= if mem (tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else (error ("P"^stringofint(pnum)^": '"^
a^"' is not an array")
handle Error => (err_cnt := (!err_cnt) + 1; []))
| ev (Event2(Name a)) tbl pnum l ct1
= if mem(tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else [] (* if it is not an array (a simple event) *)
| ev (Event3(Name a,b)) tbl pnum l ct1
= if mem (tbl,a) then [{name=a,dim=(mevbody b 0), pos=l}]
else (error ("P"^stringofint(pnum)^": '"^
a^"' is not an array")
handle Error => (err_cnt := (!err_cnt) + 1; []))
and mevbody (Empty) ct = [ct+2] @ [ct+1]
| mevbody (Meventbody1(a)) ct = []
| mevbody (Meventbody2(a)) ct = (mevbody a (ct+1)) @ [ct+1]
| mevbody (Meventbody3(a,b)) ct = mevbody b (ct+1)
| mevbody (Meventbody4(a)) ct = [ct+2]
and getlist(name,((a:Arraytable)::x))
= if name = (#name a) then count1(1,(#dim a))
else getlist(name,x)
| getlist(name,[]) = []
and count1(ini,fi)
= if ini <= fi
then (count1((ini+1),fi)) @ [ini]
else []
and check(l,tbl,pnum)
= if chk(l) then
(if samedim(l,[]) then
(error ("P"^stringofint(pnum)^
": Use same distributable dimension.")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else check1(remv(l,pnum),tbl,pnum))
else true
and chk(a::x) = if (length(#dim a) <> length(#pos a)) then false
else chk(x)
| chk [] = true
(* use same distributable dimension, for example: ;1[a,;1[b]] *)
and samedim ((a:temp1)::x,l1) = if samedim1((#pos a),l1) then true
else samedim(x,[])
| samedim ([],l1) = false
and samedim1 (a::x,l1) = if (member l1 (#d a)) andalso (#d a) <> 0
then true
else samedim1 (x,(l1 @ [(#d a)]))
| samedim1 ([],l1) = false
(*remove those which their dim is blank or those which the range
is no blank*)
and remv ((a:temp1)::x,pnum)
= if dimlist((#dim a),(#pos a),pnum) = [] then remv (x,pnum)
else [{name=(#name a),
dim=dimlist((#dim a),(#pos a),pnum),
pos=poslist(#pos a)}]
@ remv (x,pnum)
| remv ([],pnum) = []
and dimlist(dim,pos::x,pnum)
= if (#d pos) > 0 andalso not (member dim (#d pos))
then (error ("P"^stringofint(pnum)
^": '"^stringofint(#d pos)
^"' dimension is not a distributable dimension.")
handle Error => (err_cnt := (!err_cnt) + 1; []))
else if (#d pos) > 0 andalso (#p pos) <> (~1)
then [(#d pos)] @ dimlist(dim,x,pnum)
else dimlist(dim,x,pnum)
| dimlist(dim,[],pnum) = []
and poslist(pos::x) = if (#d pos) > 0 andalso (#p pos) <> (~1)
then [pos] @ poslist(x)
else poslist(x)
| poslist([]) = []
and check1(((a:temp1):: x),tbl,pnum)
= check2 (getnum((#name a),(#dim a),tbl)) x tbl pnum
(getp(#pos a)) (newlist((#name a),(#dim a),(#pos a)))
| check1([],tbl,pnum)= true
and check2 num ((a:temp1)::x) tbl pnum p l
= if p<>getp(#pos a) then check2 num x tbl pnum p (l @ [a])
else if num<>getnum((#name a),(#dim a),tbl)
then (error ("P"^stringofint(pnum)
^": Do not have the same number of sections generated by '"
^stringofint(getd(#pos a))^"' dimension")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else check2 num x tbl pnum p
(l @ (newlist((#name a),(#dim a),(#pos a))))
| check2 num [] tbl pnum p l = check1(l,tbl,pnum)
and getp (a::x) =(#p a)
| getp [] = error "Error"
and getd (a::x) =(#d a)
| getd [] = error "Error"
and newlist (name,a::x,b::y)
= if x=[] andalso y=[] then [] else [{name=name,dim=x,pos=y}]
| newlist (name,[],[]) = error "Error"
| newlist (name,l,[]) = error "Error"
| newlist (name,[],l) = error "Error"
and getnum(na,dim,((a:Arraytable)::x))
= if na <> (#name a) then getnum(na,dim,x)
else getnum1(hd(dim),(#value a))
| getnum(na,dim,[]) = 0 (*error "not an array"
handle Error => (err_cnt := (!err_cnt) + 1; 0) *)
and getnum1(dim,(v:bound)::x)
= if dim <> (#pos v) then getnum1(dim,x)
else count2 ((#lower v),(#upper v),(#step v))
| getnum1(dim,[]) = error "Error"
and count2(ini,fi,inc)
= if ini <= fi andalso inc > 0
then 1 + count2((ini+inc),fi,inc)
else if ini >= fi andalso inc < 0
then 1 + count2((ini+inc),fi,inc)
else 0
and chkdim(b,pnum) = if (iex1 b) <= 0
then (error ("P"^stringofint(pnum)
^": Dimension less or equal to zero.")
handle Error => (err_cnt := (!err_cnt) + 1; 0))
else (iex1 b)
in
fun drest22 x = dres22 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Drest3.
Drest3: Inside a k-nested distributor there must be at least one
slice event with k distributable dimensions, and no array
slices with more than k distributable dimensions *)
local
open CSY
open CSR_PRLD
open PRLD
fun dres3 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum
| mpbody (Programbody2(a)) tbl pnum = mpr a tbl pnum
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum = mseq a tbl pnum
and mpr (Process(a)) tbl pnum = mseq a tbl pnum
and brep (Bodyreplicator(a,b)) tbl pnum = bbrep b tbl pnum
and bbrep (BBodyreplicator1(a)) tbl pnum = mpa a tbl pnum
| bbrep (BBodyreplicator2(a)) tbl pnum = mpr a tbl pnum
| bbrep (BBodyreplicator3(a)) tbl pnum = brep a tbl pnum
| bbrep (BBodyreplicator4(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator5(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator6(a,b)) tbl pnum
= (brep a tbl pnum) andalso (bbrep b tbl pnum)
and mseq (Sequence1(a)) tbl pnum = morel a tbl pnum
| mseq (Sequence2(a,b)) tbl pnum
= (morel a tbl pnum) orelse (mseq b tbl pnum)
and morel (Orelement1(a)) tbl pnum = mgel a tbl pnum
| morel (Orelement2(a,b)) tbl pnum
= (mgel a tbl pnum) orelse (morel b tbl pnum)
and mgel (Gelement1(a)) tbl pnum = mstel a tbl pnum
| mgel (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel (Gelement3(a)) tbl pnum = dist a tbl pnum 1
| mgel (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel b tbl pnum)
| mgel (Gelement5(a,b)) tbl pnum
= (mstel a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_2(a,b)) tbl pnum
= (dist a tbl pnum 1) andalso (mgelL b tbl pnum)
and mgelL (GelementL1(a)) tbl pnum = lrepl a tbl pnum
| mgelL (GelementL2(a,b)) tbl pnum
= (lrepl a tbl pnum) andalso (mgelL b tbl pnum)
and dist (Distributor1(a,b,c,d)) tbl pnum num
= mseq1 d tbl pnum num
| dist (Distributor2(a,b,c)) tbl pnum num = mseq1 c tbl pnum num
| dist (Distributor3(a,b,c)) tbl pnum num = mseq1 c tbl pnum num
| dist (Distributor4(a,b)) tbl pnum num = mseq1 b tbl pnum num
and mstel (Nostar(a)) tbl pnum = mel a tbl pnum
| mstel (Star(a)) tbl pnum = mel a tbl pnum
and mel (Element(a)) tbl pnum = true
| mel (Group(a)) tbl pnum = mseq a tbl pnum
and srepl (Sreplicator1(a,b)) tbl pnum = conc b tbl pnum
| srepl (Sreplicator2(a,b)) tbl pnum = imbr b tbl pnum
and conc (Concseq(a,b)) tbl pnum = mseq a tbl pnum
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum
= (mseq a tbl pnum) andalso (mseq e tbl pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
andalso (mseq g tbl pnum)
| imbr (Imbrseq3(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq3s(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq4(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq5(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq5s(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq6(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq7(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq7s(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq8(a)) tbl pnum = imbr a tbl pnum
| imbr (Imbrseq8s(a)) tbl pnum = imbr a tbl pnum
(*| imbr (Imbrseq9(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum = conc b tbl pnum
| rrepl (Rreplicator2(a,b,c)) tbl pnum = imbr b tbl pnum
and lrepl (Lreplicator1(a,b,c)) tbl pnum = conc c tbl pnum
| lrepl (Lreplicator2(a,b,c)) tbl pnum = imbr c tbl pnum
and mseq1 (Sequence1(a)) tbl pnum num = morel1 a tbl pnum num
| mseq1 (Sequence2(a,b)) tbl pnum num
= (morel1 a tbl pnum num) orelse (mseq1 b tbl pnum num)
and morel1 (Orelement1(a)) tbl pnum num = mgel1 a tbl pnum num
| morel1 (Orelement2(a,b)) tbl pnum num
= (mgel1 a tbl pnum num) orelse (morel1 b tbl pnum num)
and mgel1 (Gelement1(a)) tbl pnum num = mstel1 a tbl pnum num
| mgel1 (Gelement2(a)) tbl pnum num = srepl a tbl pnum
| mgel1 (Gelement3(a)) tbl pnum num = dist a tbl pnum (num+1)
| mgel1 (Gelement4(a,b)) tbl pnum num
= (rrepl a tbl pnum) andalso (mgel1 b tbl pnum num)
| mgel1 (Gelement5(a,b)) tbl pnum num
= (mstel1 a tbl pnum num) andalso (mgelL b tbl pnum)
| mgel1 (Gelement5_1(a,b)) tbl pnum num
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel1 (Gelement5_2(a,b)) tbl pnum num
= (dist a tbl pnum (num+1)) andalso (mgelL b tbl pnum)
and mstel1 (Nostar(a)) tbl pnum num = mel1 a tbl pnum num
| mstel1 (Star(a)) tbl pnum num = mel1 a tbl pnum num
and mel1 (Element(a)) tbl pnum num = ev a tbl pnum num
| mel1 (Group(a)) tbl pnum num = mseq1 a tbl pnum num
and ev (Event1(Name a)) tbl pnum num
= check (tbl,pnum,a,num)
| ev (Event2(Name a)) tbl pnum num
= check (tbl,pnum,a,num)
| ev (Event3(Name a,b)) tbl pnum num
= if mem (tbl,a) then
(if num > (mevbody b 0)
then (error ("P"^stringofint(pnum)
^": No "^stringofint(num)^" distributable dimensions")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else if num < (mevbody b 0)
then (error ("P"^stringofint(pnum)
^": More then "^stringofint(num)^" distributable dimensions")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else true)
else true
and mevbody (Empty) ct = ct + 2
| mevbody (Meventbody1(a)) ct = ct
| mevbody (Meventbody2(a)) ct = mevbody a (ct+1)
| mevbody (Meventbody3(a,b)) ct = mevbody b ct
| mevbody (Meventbody4(a)) ct = ct + 1
and check ((a:Arraytable)::x,pnum,y,num)
= if (y <> (#name a)) then check (x,pnum,y,num)
else if num > (#dim a)
then (error ("P"^stringofint(pnum)
^": No "^stringofint(num)^" distributable dimensions")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else if num < (#dim a)
then (error ("P"^stringofint(pnum)
^": More then "^stringofint(num)^" distributable dimensions")
handle Error => (err_cnt := (!err_cnt) + 1; true))
else true
| check ([],pnum,y,num) = true (* false *)
in
fun drest3 x = dres3 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Drest4.
Drest4: If dim = j then every slice event with maximal number of
distributable dimesions must have the jth dimension as a
distributable dimension. *)
local
open CSY
open CSR_PRLD
open PRLD
type posl = {p : int, d : int}
type temp1 = {name : string, dim : int list, pos : posl list}
fun dres4 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum
| mpbody (Programbody2(a)) tbl pnum = mpr a tbl pnum
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum = mseq a tbl pnum
and mpr (Process(a)) tbl pnum = mseq a tbl pnum
and brep (Bodyreplicator(a,b)) tbl pnum = bbrep b tbl pnum
and bbrep (BBodyreplicator1(a)) tbl pnum = mpa a tbl pnum
| bbrep (BBodyreplicator2(a)) tbl pnum = mpr a tbl pnum
| bbrep (BBodyreplicator3(a)) tbl pnum = brep a tbl pnum
| bbrep (BBodyreplicator4(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator5(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator6(a,b)) tbl pnum
= (brep a tbl pnum) andalso (bbrep b tbl pnum)
and mseq (Sequence1(a)) tbl pnum = morel a tbl pnum
| mseq (Sequence2(a,b)) tbl pnum
= (morel a tbl pnum) orelse (mseq b tbl pnum)
and morel (Orelement1(a)) tbl pnum = mgel a tbl pnum
| morel (Orelement2(a,b)) tbl pnum
= (mgel a tbl pnum) orelse (morel b tbl pnum)
and mgel (Gelement1(a)) tbl pnum = mstel a tbl pnum
| mgel (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel (Gelement3(a)) tbl pnum
= check ((dist a tbl [] 0),tbl,pnum)
| mgel (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel b tbl pnum)
| mgel (Gelement5(a,b)) tbl pnum
= (mstel a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_2(a,b)) tbl pnum
= (check((dist a tbl [] 0),tbl,pnum))
andalso (mgelL b tbl pnum)
and mgelL (GelementL1(a)) tbl pnum = lrepl a tbl pnum
| mgelL (GelementL2(a,b)) tbl pnum
= (lrepl a tbl pnum) andalso (mgelL b tbl pnum)
and dist (Distributor1(a,b,c,d)) tbl l ct1
= mseq1 d tbl (l @ [{p=ct1+1, d=iex1 b}]) (ct1+1)
| dist (Distributor2(a,b,c)) tbl l ct1
= mseq1 c tbl (l @ [{p=ct1+1, d=iex1 b}]) (ct1+1)
| dist (Distributor3(a,b,c)) tbl l ct1
= mseq1 c tbl (l @ [{p=ct1+1, d=0}]) (ct1+1)
| dist (Distributor4(a,b)) tbl l ct1
= mseq1 b tbl (l @ [{p=ct1+1,d=0}]) (ct1+1)
and mstel (Nostar(a)) tbl pnum = mel a tbl pnum
| mstel (Star(a)) tbl pnum = mel a tbl pnum
and mel (Element(a)) tbl pnum = true
| mel (Group(a)) tbl pnum = mseq a tbl pnum
and srepl (Sreplicator1(a,b)) tbl pnum = conc b tbl pnum
| srepl (Sreplicator2(a,b)) tbl pnum = imbr b tbl pnum
and conc (Concseq(a,b)) tbl pnum = mseq a tbl pnum
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum
= (mseq a tbl pnum) andalso (mseq e tbl pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
andalso (mseq g tbl pnum)
| imbr (Imbrseq3(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq3s(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq4(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq5(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq5s(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq6(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq7(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq7s(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq8(a)) tbl pnum = imbr a tbl pnum
| imbr (Imbrseq8s(a)) tbl pnum = imbr a tbl pnum
(*| imbr (Imbrseq9(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum = conc b tbl pnum
| rrepl (Rreplicator2(a,b,c)) tbl pnum = imbr b tbl pnum
and lrepl (Lreplicator1(a,b,c)) tbl pnum = conc c tbl pnum
| lrepl (Lreplicator2(a,b,c)) tbl pnum = imbr c tbl pnum
and mseq1 (Sequence1(a)) tbl l ct1 = morel1 a tbl l ct1
| mseq1 (Sequence2(a,b)) tbl l ct1
= (morel1 a tbl l ct1) @ (mseq1 b tbl l ct1)
and morel1 (Orelement1(a)) tbl l ct1 = mgel1 a tbl l ct1
| morel1 (Orelement2(a,b)) tbl l ct1
= (mgel1 a tbl l ct1) @ (morel1 b tbl l ct1)
and mgel1 (Gelement1(a)) tbl l ct1 = mstel1 a tbl l ct1
| mgel1 (Gelement2(a)) tbl l ct1 = srepl1 a tbl l ct1
| mgel1 (Gelement3(a)) tbl l ct1 = dist a tbl l ct1
| mgel1 (Gelement4(a,b)) tbl l ct1
= (rrepl1 a tbl l ct1) @ (mgel1 b tbl l ct1)
| mgel1 (Gelement5(a,b)) tbl l ct1
= (mstel1 a tbl l ct1) @ (mgelL1 b tbl l ct1)
| mgel1 (Gelement5_1(a,b)) tbl l ct1
= (srepl1 a tbl l ct1) @ (mgelL1 b tbl l ct1)
| mgel1 (Gelement5_2(a,b)) tbl l ct1
= (dist a tbl l ct1) @ (mgelL1 b tbl l ct1)
and mgelL1 (GelementL1(a)) tbl l ct1 = lrepl1 a tbl l ct1
| mgelL1 (GelementL2(a,b)) tbl l ct1
= (lrepl1 a tbl l ct1) @ (mgelL1 b tbl l ct1)
and mstel1 (Nostar(a)) tbl l ct1 = mel1 a tbl l ct1
| mstel1 (Star(a)) tbl l ct1 = mel1 a tbl l ct1
and mel1 (Element(a)) tbl l ct1 = ev a tbl l ct1
| mel1 (Group(a)) tbl l ct1 = mseq1 a tbl l ct1
and srepl1 (Sreplicator1(a,b)) tbl l ct1 = conc1 b tbl l ct1
| srepl1 (Sreplicator2(a,b)) tbl l ct1 = imbr1 b tbl l ct1
and conc1 (Concseq(a,b)) tbl l ct1 = mseq1 a tbl l ct1
and imbr1 (Imbrseq1(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq2(a,b,c,d,e,f,g)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
@ (mseq1 g tbl l ct1)
| imbr1 (Imbrseq3(a,b)) tbl l ct1 = mseq1 b tbl l ct1
| imbr1 (Imbrseq3s(a,b)) tbl l ct1 = mseq1 b tbl l ct1
| imbr1 (Imbrseq4(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq4s(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq5(a,b)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq5s(a,b)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq6(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq6s(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq7(a)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq7s(a)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq8(a)) tbl l ct1 = imbr1 a tbl l ct1
| imbr1 (Imbrseq8s(a)) tbl l ct1 = imbr1 a tbl l ct1
(*| imbr1 (Imbrseq9(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq9s(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq10(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq10s(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq11(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq11s(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq12(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq13(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)*)
and rrepl1 (Rreplicator1(a,b,c)) tbl l ct1 = conc1 b tbl l ct1
| rrepl1 (Rreplicator2(a,b,c)) tbl l ct1 = imbr1 b tbl l ct1
and lrepl1 (Lreplicator1(a,b,c)) tbl l ct1 = conc1 c tbl l ct1
| lrepl1 (Lreplicator2(a,b,c)) tbl l ct1= imbr1 c tbl l ct1
and ev (Event1(Name a)) tbl l ct1
= if mem(tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else []
| ev (Event2(Name a)) tbl l ct1
= if mem(tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else [] (* if it is not an array (a simple event) *)
| ev (Event3(Name a,b)) tbl l ct1
= if mem (tbl,a) then [{name=a,dim=(mevbody b 0), pos=l}]
else [] (*error (a^" is not an array")
handle Error => (err_cnt := (!err_cnt) + 1; []) *)
and mevbody (Empty) ct = [ct+2] @ [ct+1]
| mevbody (Meventbody1(a)) ct = []
| mevbody (Meventbody2(a)) ct = (mevbody a (ct+1)) @ [ct+1]
| mevbody (Meventbody3(a,b)) ct = mevbody b (ct+1)
| mevbody (Meventbody4(a)) ct = [ct+2]
and getlist(name,((a:Arraytable)::x))
= if name = (#name a) then count1(1,(#dim a))
else getlist(name,x)
| getlist(name,[]) = []
and count1(ini,fi)
= if ini <= fi
then (count1((ini+1),fi)) @ [ini]
else []
and check(l,tbl,pnum)
= if chk(l) then
(if samedim(l,[]) then true
(*error ("P"^stringofint(pnum)^
": Use same distributable dimension")
handle Error => (err_cnt := (!err_cnt) + 1; true)*)
else check1(l,tbl,pnum))
else true
and chk(a::x) = if (length(#dim a) <> length(#pos a)) then false
else chk(x)
| chk [] = true
(* use same distributable dimension, for example: ;1[a,;1[b]] *)
and samedim ((a:temp1)::x,l1) = if samedim1((#pos a),l1) then true
else samedim(x,[])
| samedim ([],l1) = false
and samedim1 (a::x,l1)
= if (member l1 (#d a)) andalso (#d a) <> 0 then true
else samedim1 (x,(l1 @ [(#d a)]))
| samedim1 ([],l1) = false
and check1(((a:temp1):: x),tbl,pnum)
= if check2 ((#dim a),(#pos a)) then check1(x,tbl,pnum)
else true
(*(error ("P"^stringofint(pnum)
^": jth dimension is not a distributable dimension")
handle Error => (err_cnt := (!err_cnt) + 1; true)) *)
| check1([],tbl,pnum)= true
and check2(dim,a::x)
= if check3(dim,(#d a)) then check2(dim,x)
else false
| check2(dim,[]) = true
and check3(dim,d)
= if d = 0 then true else member dim d
in
fun drest4 x = dres4 x
end;
(* The following program which is between the 'local' and 'end'
is used to check the COSY program if it satisfies the Drest5.1
and Drest5.2.
Drest5.1: If range = #i1,i2,i3, dim is blank and i1,i2,i3 are
integers, then i2>=i1>=1, i3>=1 and i2 must be smaller
than or equal to the number of sections generated by
the rightmost distributable (current) dimension of any
slice event occurring in msequence.
Drest5.2: If range = #i1,i2,i3, dim = j and i1,i2,i3,j are
integers, then i2>=i1>=1, i3>=1 and i2 must be smaller
than or equal to the number of sections generated by
the jth dimension of any slice event occurring in
msequence which has the jth dimension distributable. *)
local
open CSY
open CSR_PRLD
open PRLD
type posl = {p : int, d : int, no_of_dim : int}
type temp1 = {name : string, dim : int list, pos : posl list}
fun dres5152 (Program(a)) = (mpbody a) (mktbl (Program(a))) 1
and mpbody (Programbody1(a)) tbl pnum = mpa a tbl pnum
| mpbody (Programbody2(a)) tbl pnum= mpr a tbl pnum
| mpbody (Programbody3(a)) tbl pnum = brep a tbl pnum
| mpbody (Programbody4(a,b)) tbl pnum = mpbody b tbl pnum
| mpbody (Programbody5(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody6(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (mpbody b tbl (pnum+1))
| mpbody (Programbody7(a,b)) tbl pnum
= (brep a tbl pnum) andalso (mpbody b tbl (pnum+1))
and mpa (Path(a)) tbl pnum = mseq a tbl pnum
and mpr (Process(a)) tbl pnum = mseq a tbl pnum
and brep (Bodyreplicator(a,b)) tbl pnum = bbrep b tbl pnum
and bbrep (BBodyreplicator1(a)) tbl pnum = mpa a tbl pnum
| bbrep (BBodyreplicator2(a)) tbl pnum = mpr a tbl pnum
| bbrep (BBodyreplicator3(a)) tbl pnum = brep a tbl pnum
| bbrep (BBodyreplicator4(a,b)) tbl pnum
= (mpa a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator5(a,b)) tbl pnum
= (mpr a tbl pnum) andalso (bbrep b tbl pnum)
| bbrep (BBodyreplicator6(a,b)) tbl pnum
= (brep a tbl pnum) andalso (bbrep b tbl pnum)
and mseq (Sequence1(a)) tbl pnum = morel a tbl pnum
| mseq (Sequence2(a,b)) tbl pnum
= (morel a tbl pnum) orelse (mseq b tbl pnum)
and morel (Orelement1(a)) tbl pnum = mgel a tbl pnum
| morel (Orelement2(a,b)) tbl pnum
= (mgel a tbl pnum) orelse (morel b tbl pnum)
and mgel (Gelement1(a)) tbl pnum = mstel a tbl pnum
| mgel (Gelement2(a)) tbl pnum = srepl a tbl pnum
| mgel (Gelement3(a)) tbl pnum
= check ((dist a tbl pnum [] 0),tbl,pnum)
| mgel (Gelement4(a,b)) tbl pnum
= (rrepl a tbl pnum) andalso (mgel b tbl pnum)
| mgel (Gelement5(a,b)) tbl pnum
= (mstel a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_1(a,b)) tbl pnum
= (srepl a tbl pnum) andalso (mgelL b tbl pnum)
| mgel (Gelement5_2(a,b)) tbl pnum
= (check((dist a tbl pnum [] 0),tbl,pnum))
andalso (mgelL b tbl pnum)
and mgelL (GelementL1(a)) tbl pnum = lrepl a tbl pnum
| mgelL (GelementL2(a,b)) tbl pnum
= (lrepl a tbl pnum) andalso (mgelL b tbl pnum)
and dist (Distributor1(a,b,c,d)) tbl pnum l ct1
= if range(c) then (mseq1 d tbl pnum
(l @ rangelist(iex1 b,c,ct1+1)) (ct1+1))
else (error ("P"^stringofint(pnum)^": i1,i2,i3 have problems")
handle Error => (err_cnt := (!err_cnt) + 1;
(mseq1 d tbl pnum (l @ rangelist(iex1 b,c,ct1+1)) (ct1+1))))
| dist (Distributor2(a,b,c)) tbl pnum l ct1
= mseq1 c tbl pnum (l @ [{p=ct1+1, d=iex1 b, no_of_dim=0}])
(ct1+1)
| dist (Distributor3(a,b,c)) tbl pnum l ct1
= if range(b) then mseq1 c tbl pnum
(l @ rangelist(0,b,ct1+1)) (ct1+1)
else (error ("P"^stringofint(pnum)^": i1,i2,i3 have problems")
handle Error => (err_cnt := (!err_cnt) + 1;
(mseq1 c tbl pnum (l @ rangelist(0,b,ct1+1)) (ct1+1))))
| dist (Distributor4(a,b)) tbl pnum l ct1
= mseq1 b tbl pnum (l @ [{p=ct1+1,d=0, no_of_dim=0}])
(ct1+1)
and mstel (Nostar(a)) tbl pnum = mel a tbl pnum
| mstel (Star(a)) tbl pnum = mel a tbl pnum
and mel (Element(a)) tbl pnum = true
| mel (Group(a)) tbl pnum = mseq a tbl pnum
and srepl (Sreplicator1(a,b)) tbl pnum = conc b tbl pnum
| srepl (Sreplicator2(a,b)) tbl pnum = imbr b tbl pnum
and conc (Concseq(a,b)) tbl pnum = mseq a tbl pnum
and imbr (Imbrseq1(a,b,c,d,e)) tbl pnum
= (mseq a tbl pnum) andalso (mseq e tbl pnum)
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
andalso (mseq g tbl pnum)
| imbr (Imbrseq3(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq3s(a,b)) tbl pnum = mseq b tbl pnum
| imbr (Imbrseq4(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq4s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq5(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq5s(a,b)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq6(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq6s(a,b,c,d)) tbl pnum
= (mseq a tbl pnum) andalso (mseq d tbl pnum)
| imbr (Imbrseq7(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq7s(a)) tbl pnum = mseq a tbl pnum
| imbr (Imbrseq8(a)) tbl pnum = imbr a tbl pnum
| imbr (Imbrseq8s(a)) tbl pnum = imbr a tbl pnum
(*| imbr (Imbrseq9(a,b,c)) tbl pnum
= (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl = (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl = (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (mseq a tbl) andalso (imbr c tbl) andalso (mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl = (mseq a tbl) andalso (imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl) andalso (mseq c tbl)*)
and mseq1 (Sequence1(a)) tbl pnum l ct1 = morel1 a tbl pnum l ct1
| mseq1 (Sequence2(a,b)) tbl pnum l ct1
= (morel1 a tbl pnum l ct1) @ (mseq1 b tbl pnum l ct1)
and morel1 (Orelement1(a)) tbl pnum l ct1 = mgel1 a tbl pnum l ct1
| morel1 (Orelement2(a,b)) tbl pnum l ct1
= (mgel1 a tbl pnum l ct1) @ (morel1 b tbl pnum l ct1)
and mgel1 (Gelement1(a)) tbl pnum l ct1 = mstel1 a tbl pnum l ct1
| mgel1 (Gelement2(a)) tbl pnum l ct1 = srepl1 a tbl pnum l ct1
| mgel1 (Gelement3(a)) tbl pnum l ct1 = dist a tbl pnum l ct1
| mgel1 (Gelement4(a,b)) tbl pnum l ct1
= (rrepl1 a tbl pnum l ct1) @ (mgel1 b tbl pnum l ct1)
| mgel1 (Gelement5(a,b)) tbl pnum l ct1
= (mstel1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
| mgel1 (Gelement5_1(a,b)) tbl pnum l ct1
= (srepl1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
| mgel1 (Gelement5_2(a,b)) tbl pnum l ct1
= (dist a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
and mgelL1 (GelementL1(a)) tbl pnum l ct1 = lrepl1 a tbl pnum l ct1
| mgelL1 (GelementL2(a,b)) tbl pnum l ct1
= (lrepl1 a tbl pnum l ct1) @ (mgelL1 b tbl pnum l ct1)
and mstel1 (Nostar(a)) tbl pnum l ct1 = mel1 a tbl pnum l ct1
| mstel1 (Star(a)) tbl pnum l ct1 = mel1 a tbl pnum l ct1
and mel1 (Element(a)) tbl pnum l ct1 = ev a tbl pnum l ct1
| mel1 (Group(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
and srepl1 (Sreplicator1(a,b)) tbl pnum l ct1
= conc1 b tbl pnum l ct1
| srepl1 (Sreplicator2(a,b)) tbl pnum l ct1
= imbr1 b tbl pnum l ct1
and conc1 (Concseq(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
and imbr1 (Imbrseq1(a,b,c,d,e)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 e tbl pnum l ct1)
| imbr1 (Imbrseq2(a,b,c,d,e,f,g)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1) @
(mseq1 g tbl pnum l ct1)
| imbr1 (Imbrseq3(a,b)) tbl pnum l ct1 = mseq1 b tbl pnum l ct1
| imbr1 (Imbrseq3s(a,b)) tbl pnum l ct1 = mseq1 b tbl pnum l ct1
| imbr1 (Imbrseq4(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq4s(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq5(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq5s(a,b)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq6(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq6s(a,b,c,d)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (mseq1 d tbl pnum l ct1)
| imbr1 (Imbrseq7(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq7s(a)) tbl pnum l ct1 = mseq1 a tbl pnum l ct1
| imbr1 (Imbrseq8(a)) tbl pnum l ct1 = imbr1 a tbl pnum l ct1
| imbr1 (Imbrseq8s(a)) tbl pnum l ct1 = imbr1 a tbl pnum l ct1
(*| imbr1 (Imbrseq9(a,b,c)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (imbr1 c tbl pnum l ct1)
| imbr1 (Imbrseq9s(a,b,c)) tbl pnum l ct1
= (mseq1 a tbl pnum l ct1) @ (imbr1 c tbl pnum l ct1)
| imbr1 (Imbrseq10(a,b,c)) tbl pnum l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl pnum l ct1)
| imbr1 (Imbrseq10s(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq11(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq11s(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq12(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq13(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)*)
and rrepl (Rreplicator1(a,b,c)) tbl pnum = conc b tbl pnum
| rrepl (Rreplicator2(a,b,c)) tbl pnum = imbr b tbl pnum
and rrepl1 (Rreplicator1(a,b,c)) tbl pnum l ct1
= conc1 b tbl pnum l ct1
| rrepl1 (Rreplicator2(a,b,c)) tbl pnum l ct1
= imbr1 b tbl pnum l ct1
and lrepl (Lreplicator1(a,b,c)) tbl pnum = conc c tbl pnum
| lrepl (Lreplicator2(a,b,c)) tbl pnum = imbr c tbl pnum
and lrepl1 (Lreplicator1(a,b,c)) tbl pnum l ct1
= conc1 c tbl pnum l ct1
| lrepl1 (Lreplicator2(a,b,c)) tbl pnum l ct1
= imbr1 c tbl pnum l ct1
and ev (Event1(Name a)) tbl pnum l ct1
= if mem(tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else []
| ev (Event2(Name a)) tbl pnum l ct1
= if mem(tbl,a) then [{name=a, dim=getlist(a,tbl), pos=l}]
else [] (* if it is not an array (a simple event) *)
| ev (Event3(Name a,b)) tbl pnum l ct1
= if mem (tbl,a) then [{name=a,dim=(mevbody b 0), pos=l}]
else [] (*error "not an array"*)
and mevbody (Empty) ct = [ct+2] @ [ct+1]
| mevbody (Meventbody1(a)) ct = []
| mevbody (Meventbody2(a)) ct = (mevbody a (ct+1)) @ [ct+1]
| mevbody (Meventbody3(a,b)) ct = mevbody b (ct+1)
| mevbody (Meventbody4(a)) ct = [ct+2]
and getlist(nname,((a:Arraytable)::x))
= if nname = (#name a) then count1(1,(#dim a))
else getlist(nname,x)
| getlist(nname,[]) = []
and count1(ini,fi)
= if ini <= fi
then (count1((ini+1),fi)) @ [ini]
else []
and range(Range(a,b,c))
= if cmp(iex a, iex b, iex c) then true
else false
and cmp(a,b,c)
= if a >= 1 andalso b >= 1 andalso c >= 1 andalso b >= a
then true else false
and rangelist(dim,Range(a,b,c),cnt)
= [{p=cnt, d=dim, no_of_dim=(count2(iex a,iex b,iex c))}]
and check(l,tbl,pnum)
= if chk(l) then check1(remv(l),tbl,pnum)
else true
and chk(a::x) = if (length(#dim a) <> length(#pos a)) then false
else chk(x)
| chk [] = true
(* remove those which their dim is blank *)
and remv ((a:temp1)::x)
= if dimlist((#dim a),(#pos a)) = [] then remv x
else [{name=(#name a),
dim=dimlist((#dim a),(#pos a)),
pos=poslist(#pos a)}]
@ remv x
| remv [] = []
and dimlist(dim,pos::x)
= if (#no_of_dim pos) > 0 andalso (#d pos) = 0
then [hd(dim)] @ dimlist(tl(dim),x)
else if (#no_of_dim pos) > 0 andalso (#d pos) > 0
then dimlist2(dim,(#d pos))
@ dimlist(dimlist1(dim,(#d pos)),x)
else if (#no_of_dim pos) = 0 andalso (#d pos) > 0
then dimlist(dimlist1(dim,(#d pos)),x)
else dimlist(tl(dim),x)
| dimlist(dim,[]) = dim
and dimlist1(dim::x,d) = if d = dim
then dimlist1(x,d)
else [dim] @ dimlist1(x,d)
| dimlist1([],d) = []
and dimlist2(dim,d) = if member dim d then [d]
else []
(*(error "do not have the jth distributable dimension"
handle Error => (err_cnt := (!err_cnt) + 1; []))*)
and poslist(pos::x) = if (#no_of_dim pos) > 0
then [pos] @ poslist(x)
else poslist(x)
| poslist([]) = []
and check1(((a:temp1)::x),tbl,pnum)
= if check2 ((#name a),(#dim a),(#pos a),tbl)
then check1(x,tbl,pnum)
else (error ("P"^stringofint(pnum)
^": Range is out of boundary")
handle Error => (err_cnt := (!err_cnt) + 1; true))
| check1([],tbl,pnum)= true
and check2 (name,dim::x,pos::y,tbl)
= if getnum(name,dim,tbl) >= (#no_of_dim pos)
then check2(name,x,y,tbl)
else false
| check2 (name,[],[],tbl) = true
| check2 (name,x,[],tbl) = true
| check2 (name,[],y,tbl) = true
and getnum(na,dim,((a:Arraytable)::x))
= if na <> (#name a) then getnum(na,dim,x)
else getnum1(dim,(#value a))
| getnum(na,dim,[]) = 0 (*error "not an array"
handle Error => (err_cnt := (!err_cnt) + 1; 0)*)
and getnum1(dim,(v:bound)::x)
= if dim <> (#pos v) then getnum1(dim,x)
else count2 ((#lower v),(#upper v),(#step v))
| getnum1(dim,[]) = error "Error2"
and count2(ini,fi,inc)
= if ini <= fi andalso inc > 0
then 1 + count2((ini+inc),fi,inc)
else if ini >= fi andalso inc < 0
then 1 + count2((ini+inc),fi,inc)
else 0
in
fun drest5152 x = dres5152 x
end;
end
(* end of file `csr.sml' *)
(* File name: transform.sml
Objective: This program will check the whole tree and change the
distributor sub-trees into concatenator sub-trees.
Input : mprogram
Output : mprogram *)
functor Transform(structure CSY: COSY
structure PRLD: PRELUDE
structure CSR_PRLD: CSR_PRELUDE
structure CSR: CSR
sharing CSR.CSY = CSY = CSR_PRLD.CSY): TRANSFORM =
struct
structure CSY = CSY
structure PRLD = PRLD
structure CSR_PRLD = CSR_PRLD
structure CSR = CSR
type bound = CSR.bound
type Arraytable = CSR.Arraytable
local
open CSY
open PRLD
open CSR_PRLD
open CSR
type bound = {pos : int,
lower : int,
upper : int,
step : int}
type Arraytable = {name : string,
dim : int,
value : bound list}
fun trans (Program(a)) = Program(s_mpb a (mktbl(Program(a))))
and s_mpb (Programbody1(a)) tbl = Programbody1(s_mpa a tbl)
| s_mpb (Programbody2(a)) tbl = Programbody2(s_mpr a tbl)
| s_mpb (Programbody3(a)) tbl = Programbody3(s_brep a tbl)
| s_mpb (Programbody4(a,b)) tbl
= Programbody4(a,(s_mpb b tbl))
| s_mpb (Programbody5(a,b)) tbl
= Programbody5((s_mpa a tbl),(s_mpb b tbl))
| s_mpb (Programbody6(a,b)) tbl
= Programbody6((s_mpr a tbl),(s_mpb b tbl))
| s_mpb (Programbody7(a,b)) tbl
= Programbody7((s_brep a tbl),(s_mpb b tbl))
and s_mpa (Path(a)) tbl = Path(s_mseq a tbl)
and s_mpr (Process(a)) tbl = Process(s_mseq a tbl)
and s_brep (Bodyreplicator(a,b)) tbl
= Bodyreplicator(a,(bbrep b tbl))
and bbrep (BBodyreplicator1(a)) tbl
= BBodyreplicator1(s_mpa a tbl)
| bbrep (BBodyreplicator2(a)) tbl
= BBodyreplicator2(s_mpr a tbl)
| bbrep (BBodyreplicator3(a)) tbl
= BBodyreplicator3(s_brep a tbl)
| bbrep (BBodyreplicator4(a,b)) tbl
= BBodyreplicator4((s_mpa a tbl),(bbrep b tbl))
| bbrep (BBodyreplicator5(a,b)) tbl
= BBodyreplicator5((s_mpr a tbl),(bbrep b tbl))
| bbrep (BBodyreplicator6(a,b)) tbl
= BBodyreplicator6((s_brep a tbl),(bbrep b tbl))
and s_mseq (Sequence1(a)) tbl = Sequence1(s_mor a tbl)
| s_mseq (Sequence2(a,b)) tbl
= Sequence2((s_mor a tbl),(s_mseq b tbl))
and s_mor (Orelement1(a)) tbl = Orelement1(s_gel a tbl)
| s_mor (Orelement2(a,b)) tbl
= Orelement2((s_gel a tbl),(s_mor b tbl))
and s_gel (Gelement1(a)) tbl = Gelement1(s_mstel a tbl)
| s_gel (Gelement2(a)) tbl = Gelement2(s_srepl a tbl)
| s_gel (Gelement3(a)) tbl
= Gelement2(dist a tbl 1 (distlst a tbl [] 0))
| s_gel (Gelement4(a,b)) tbl
= Gelement4((s_rrepl a tbl),(s_gel b tbl))
| s_gel (Gelement5(a,b)) tbl
= Gelement5((s_mstel a tbl),(s_gelL b tbl))
| s_gel (Gelement5_1(a,b)) tbl
= Gelement5_1((s_srepl a tbl),(s_gelL b tbl))
| s_gel (Gelement5_2(a,b)) tbl
= Gelement5_1((dist a tbl 1 (distlst a tbl [] 0)),
(s_gelL b tbl))
and s_gelL (GelementL1(a)) tbl = GelementL1(s_lrepl a tbl)
| s_gelL (GelementL2(a,b)) tbl
= GelementL2((s_lrepl a tbl),(s_gelL b tbl))
and s_srepl (Sreplicator1(a,b)) tbl
= Sreplicator1(a,(s_conc b tbl))
| s_srepl (Sreplicator2(a,b)) tbl
= Sreplicator2(a,(s_imbr b tbl))
and s_rrepl (Rreplicator1(a,b,c)) tbl
= Rreplicator1(a,(s_conc b tbl),c)
| s_rrepl (Rreplicator2(a,b,c)) tbl
= Rreplicator2(a,(s_imbr b tbl),c)
and s_lrepl (Lreplicator1(a,b,c)) tbl
= Lreplicator1(a,b,(s_conc c tbl))
| s_lrepl (Lreplicator2(a,b,c)) tbl
= Lreplicator2(a,b,(s_imbr c tbl))
and s_mstel (Nostar(a)) tbl = Nostar(s_mel a tbl)
| s_mstel (Star(a)) tbl = Star(s_mel a tbl)
and s_mel (Element(a)) tbl = Element(s_mev a tbl)
| s_mel (Group(a)) tbl = Group(s_mseq a tbl)
and s_mev (Event1(a)) tbl = Event1(a)
| s_mev (Event2(a)) tbl = Event2(a)
| s_mev (Event3(a,b)) tbl = Event3(a,b)
and s_conc (Concseq(a,b)) tbl = Concseq((s_mseq a tbl),b)
and s_imbr (Imbrseq1(a,b,c,d,e)) tbl
= Imbrseq1((s_mseq a tbl),b,c,d,(s_mseq e tbl))
| s_imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl
= Imbrseq2((s_mseq a tbl),b,c,(s_mseq d tbl),e,f,
(s_mseq g tbl))
| s_imbr (Imbrseq3(a,b)) tbl = Imbrseq3(a,(s_mseq b tbl))
| s_imbr (Imbrseq3s(a,b)) tbl = Imbrseq3s(a,(s_mseq b tbl))
| s_imbr (Imbrseq4(a,b,c,d)) tbl
= Imbrseq4((s_mseq a tbl),b,c,(s_mseq d tbl))
| s_imbr (Imbrseq4s(a,b,c,d)) tbl
= Imbrseq4s((s_mseq a tbl),b,c,(s_mseq d tbl))
| s_imbr (Imbrseq5(a,b)) tbl = Imbrseq5((s_mseq a tbl),b)
| s_imbr (Imbrseq5s(a,b)) tbl = Imbrseq5s((s_mseq a tbl),b)
| s_imbr (Imbrseq6(a,b,c,d)) tbl
= Imbrseq6((s_mseq a tbl),b,c,(s_mseq d tbl))
| s_imbr (Imbrseq6s(a,b,c,d)) tbl
= Imbrseq6s((s_mseq a tbl),b,c,(s_mseq d tbl))
| s_imbr (Imbrseq7(a)) tbl = Imbrseq7(s_mseq a tbl)
| s_imbr (Imbrseq7s(a)) tbl = Imbrseq7s(s_mseq a tbl)
| s_imbr (Imbrseq8(a)) tbl = Imbrseq8(s_imbr a tbl)
| s_imbr (Imbrseq8s(a)) tbl = Imbrseq8s(s_imbr a tbl)
(*| s_imbr (Imbrseq9(a,b,c)) tbl
= Imbrseq9((s_mseq a tbl),b,(s_imbr c tbl))
| s_imbr (Imbrseq9s(a,b,c)) tbl
= Imbrseq9s((s_mseq a tbl),b,(s_imbr c tbl))
| s_imbr (Imbrseq10(a,b,c)) tbl
= Imbrseq10((s_imbr a tbl),b,(s_mseq c tbl))
| s_imbr (Imbrseq10s(a,b,c)) tbl
= Imbrseq10s((s_imbr a tbl),b,(s_mseq c tbl))
| s_imbr (Imbrseq11(a,b,c,d,e)) tbl
= Imbrseq11((s_mseq a tbl),b,(s_imbr c tbl),d,
(s_mseq e tbl))
| s_imbr (Imbrseq11s(a,b,c,d,e)) tbl
= Imbrseq11s((s_mseq a tbl),b,(s_imbr c tbl),d,
(s_mseq e tbl))
| s_imbr (Imbrseq12(a,b,c)) tbl
= Imbrseq12((s_mseq a tbl),b,(s_imbr c tbl))
| s_imbr (Imbrseq13(a,b,c)) tbl
= Imbrseq13((s_imbr a tbl),b,(s_mseq c tbl))*)
and dist (Distributor4(a,b)) tbl num lst
= Sreplicator1(Range_spec(Indexvariable(Name
(stringofint(num))),
Iexpr1(Integer 1),Iexpr1(Integer (getm(num,lst,tbl,lst))),
Iexpr1(Integer 1)), Concseq((s_mseq1 b tbl num lst),a))
| dist (Distributor2(a,b,c)) tbl num lst
= Sreplicator1(Range_spec(Indexvariable
(Name(stringofint(num))),
Iexpr1(Integer 1),Iexpr1(Integer (getm(num,lst,tbl,lst))),
Iexpr1(Integer 1)),Concseq((s_mseq1 c tbl num lst),a))
| dist (Distributor3(a,b,c)) tbl num lst
= Sreplicator1(Range_spec(Indexvariable(Name
(stringofint(num))),
rang1(b),rang2(b),rang3(b)),
Concseq((s_mseq1 c tbl num lst),a))
| dist (Distributor1(a,b,c,d)) tbl num lst
= Sreplicator1(Range_spec(Indexvariable(Name
(stringofint(num))),
rang1(c),rang2(c),rang3(c)),
Concseq((s_mseq1 d tbl num lst),a))
and rang1(Range(a,b,c)) = a
and rang2(Range(a,b,c)) = b
and rang3(Range(a,b,c)) = c
and getpos(num,a::x)
= if chk(num,(#pos a))
then getp(num,(#dim a),(#dim a),
getd(num,(#pos a)),(#pos a),1)
else getpos(num,x)
| getpos(num,[]) = error "Impossible" handle Error => 0
and chk(num,a::x)
= if num = (#p a) then true else chk(num,x)
| chk(num,[]) = false
and getd(num,a::x)
= if num = (#p a) then (#d a) else getd(num,x)
| getd(num,[]) = error "Impossible"
and getp(num,a::x,dimlst,dim,pos,i)
= if dim <> 0 then dim
else if num=i then a
else getp1(cntnum(num,pos,0),remv1(num,pos,dimlst),1)
| getp(num,[],dimlst,dim,pos,i)
= error "Impossible" handle Error => 0
and getp1(num,a::x,i) = if num = i then a else getp1(num,x,i+1)
| getp1(num,[],i) = error "Impossible" handle Error => 0
and cntnum(num,a::x,i)
= if num = (#p a) then (num-i)
else if (#d a) <> 0
then cntnum(num,x,i+1) else cntnum(num,x,i)
| cntnum(num,[],i) = error "Impossible" handle Error => 0
and remv1(num,a::x,dimlst)
= if num = (#p a) then dimlst
else if (#d a) <> 0
then remv1(num,x,(remv2(dimlst,(#d a))))
else remv1(num,x,dimlst)
| remv1(num,[],dimlst)
= error "Impossible" handle Error => []
and remv2(a::x,d) = if a = d then x else [a] @ remv2(x,d)
| remv2([],d) = error "Impossible" handle Error => []
and getm(num,a::x,tbl,lst)
= if chk(num,(#pos a))
then getm1(getpos(num,lst),(#name a),tbl)
else getm(num,x,tbl,lst)
| getm(num,[],tbl,lst)
= error "Impossible" handle Error => 0
and getm1(num,name,a::x)
= if name = (#name a)
then getm2(num,(#value a)) else getm1(num,name,x)
| getm1(num,name,[]) = error "Impossible" handle Error => 0
and getm2(num,a::x) = if num = (#pos a)
then ((#upper a)-(#lower a)) div (#step a) + 1
else getm2(num,x)
| getm2(num,[]) = error "Impossible" handle Error => 0
and s_mseq1 (Sequence1(a)) tbl num lst
= Sequence1(s_mor1 a tbl num lst)
| s_mseq1 (Sequence2(a,b)) tbl num lst
= Sequence2((s_mor1 a tbl num lst),
(s_mseq1 b tbl num lst))
and s_mor1 (Orelement1(a)) tbl num lst
= Orelement1(s_gel1 a tbl num lst)
| s_mor1 (Orelement2(a,b)) tbl num lst
= Orelement2((s_gel1 a tbl num lst),
(s_mor1 b tbl num lst))
and s_gel1 (Gelement1(a)) tbl num lst
= Gelement1(s_mstel1 a tbl num lst)
| s_gel1 (Gelement2(a)) tbl num lst
= Gelement2(s_srepl1 a tbl num lst)
| s_gel1 (Gelement3(a)) tbl num lst
= Gelement2(dist a tbl (num+1) lst)
| s_gel1 (Gelement4(a,b)) tbl num lst
= Gelement4((s_rrepl1 a tbl num lst),
(s_gel1 b tbl num lst))
| s_gel1 (Gelement5(a,b)) tbl num lst
= Gelement5((s_mstel1 a tbl num lst),
(s_gelL1 b tbl num lst))
| s_gel1 (Gelement5_1(a,b)) tbl num lst
= Gelement5_1((s_srepl1 a tbl num lst),
(s_gelL1 b tbl num lst))
| s_gel1 (Gelement5_2(a,b)) tbl num lst
= Gelement5_1((dist a tbl (num+1) lst),
(s_gelL1 b tbl (num+1) lst))
and s_gelL1 (GelementL1(a)) tbl num lst
= GelementL1(s_lrepl1 a tbl num lst)
| s_gelL1 (GelementL2(a,b)) tbl num lst
= GelementL2((s_lrepl1 a tbl num lst),
(s_gelL1 b tbl num lst))
and s_srepl1 (Sreplicator1(a,b)) tbl num lst
= Sreplicator1(a,(s_conc1 b tbl num lst))
| s_srepl1 (Sreplicator2(a,b)) tbl num lst
= Sreplicator2(a,(s_imbr1 b tbl num lst))
and s_rrepl1 (Rreplicator1(a,b,c)) tbl num lst
= Rreplicator1(a,(s_conc1 b tbl num lst),c)
| s_rrepl1 (Rreplicator2(a,b,c)) tbl num lst
= Rreplicator2(a,(s_imbr1 b tbl num lst),c)
and s_lrepl1 (Lreplicator1(a,b,c)) tbl num lst
= Lreplicator1(a,b,(s_conc1 c tbl num lst))
| s_lrepl1 (Lreplicator2(a,b,c)) tbl num lst
= Lreplicator2(a,b,(s_imbr1 c tbl num lst))
and s_mstel1 (Nostar(a)) tbl num lst
= Nostar(s_mel1 a tbl num lst)
| s_mstel1 (Star(a)) tbl num lst
= Star(s_mel1 a tbl num lst)
and s_mel1 (Element(a)) tbl num lst
= Element(s_mev1 a tbl num lst)
| s_mel1 (Group(a)) tbl num lst
= Group(s_mseq1 a tbl num lst)
and s_mev1 (Event1(a)) tbl num lst
= if chkmem((na1 a),lst)
then Event3(a,mbody(a,tbl,lst,num))
else Event2(na a)
| s_mev1 (Event2(a)) tbl num lst = if chkmem((na1 a),lst)
then Event3(a,mbody(a,tbl,lst,num))
else Event2(na a)
| s_mev1 (Event3(a,b)) tbl num lst
= if chkevb(b) then Event3(a,mbody(a,tbl,lst,num))
else Event3(a,(s_mbody b tbl num lst (na1 a) 1))
and chkevb (Empty) = true
| chkevb (Meventbody2 a) = chkevb a
| chkevb other = false
and s_mbody (Meventbody2(a)) tbl num lst name cnt
= Meventbody3((norform(cnt,tbl,name,
chkd(cnt,num,lst,lst))),
(s_mbody a tbl (num-1) lst name (cnt+1)))
| s_mbody(Meventbody1(a)) tbl num lst name cnt
= Meventbody1(a)
| s_mbody(Meventbody4(a)) tbl num lst name cnt
= Meventbody3(a,Meventbody1(norform(cnt+1,tbl,name,
chkd(cnt+1,num,lst,lst))))
| s_mbody(Empty) tbl num lst name cnt
= Meventbody3((norform(cnt,tbl,name,
chkd(cnt,num,lst,lst))),
Meventbody1((norform(cnt+1,tbl,name,
chkd(cnt+1,num-1,lst,lst)))))
| s_mbody(Meventbody3(a,b)) tbl num lst name cnt
= Meventbody3(a,(s_mbody b tbl (num)
lst name (cnt+1)))
and s_conc1 (Concseq(a,b)) tbl num lst
= Concseq((s_mseq1 a tbl num lst),b)
and s_imbr1 (Imbrseq1(a,b,c,d,e)) tbl num lst
= Imbrseq1((s_mseq1 a tbl num lst),b,c,d,
(s_mseq1 e tbl num lst))
| s_imbr1 (Imbrseq2(a,b,c,d,e,f,g)) tbl num lst
= Imbrseq2((s_mseq1 a tbl num lst),b,c,
(s_mseq1 d tbl num lst),e,f,(s_mseq1 g tbl num lst))
| s_imbr1 (Imbrseq3(a,b)) tbl num lst
= Imbrseq3(a,(s_mseq1 b tbl num lst))
| s_imbr1 (Imbrseq3s(a,b)) tbl num lst
= Imbrseq3s(a,(s_mseq1 b tbl num lst))
| s_imbr1 (Imbrseq4(a,b,c,d)) tbl num lst
= Imbrseq4((s_mseq1 a tbl num lst),b,c,
(s_mseq1 d tbl num lst))
| s_imbr1 (Imbrseq4s(a,b,c,d)) tbl num lst
= Imbrseq4s((s_mseq1 a tbl num lst),b,c,
(s_mseq1 d tbl num lst))
| s_imbr1 (Imbrseq5(a,b)) tbl num lst
= Imbrseq5((s_mseq1 a tbl num lst),b)
| s_imbr1 (Imbrseq5s(a,b)) tbl num lst
= Imbrseq5s((s_mseq1 a tbl num lst),b)
| s_imbr1 (Imbrseq6(a,b,c,d)) tbl num lst
= Imbrseq6((s_mseq1 a tbl num lst),b,c,
(s_mseq1 d tbl num lst))
| s_imbr1 (Imbrseq6s(a,b,c,d)) tbl num lst
= Imbrseq6s((s_mseq1 a tbl num lst),b,c,
(s_mseq1 d tbl num lst))
| s_imbr1 (Imbrseq7(a)) tbl num lst
= Imbrseq7(s_mseq1 a tbl num lst)
| s_imbr1 (Imbrseq7s(a)) tbl num lst
= Imbrseq7s(s_mseq1 a tbl num lst)
| s_imbr1 (Imbrseq8(a)) tbl num lst
= Imbrseq8(s_imbr1 a tbl num lst)
| s_imbr1 (Imbrseq8s(a)) tbl num lst
= Imbrseq8s(s_imbr1 a tbl num lst)
(*| s_imbr1 (Imbrseq9(a,b,c)) tbl num lst
= Imbrseq9((s_mseq1 a tbl num lst),b,
(s_imbr1 c tbl num lst))
| s_imbr1 (Imbrseq9s(a,b,c)) tbl num lst
= Imbrseq9s((s_mseq1 a tbl num lst),b,
(s_imbr1 c tbl num lst))
| s_imbr1 (Imbrseq10(a,b,c)) tbl num lst
= Imbrseq10((s_imbr1 a tbl num lst),b,
(s_mseq1 c tbl num lst))
| s_imbr1 (Imbrseq10s(a,b,c)) tbl num lst
= Imbrseq10s((s_imbr1 a tbl num lst),b,
(s_mseq1 c tbl num lst))
| s_imbr1 (Imbrseq11(a,b,c,d,e)) tbl num lst
= Imbrseq11((s_mseq1 a tbl num lst),b,
(s_imbr1 c tbl num lst),d,(s_mseq1 e tbl num lst))
| s_imbr1 (Imbrseq11s(a,b,c,d,e)) tbl num lst
= Imbrseq11s((s_mseq1 a tbl num lst),b,
(s_imbr1 c tbl num lst),d,(s_mseq1 e tbl num lst))
| s_imbr1 (Imbrseq12(a,b,c)) tbl num lst
= Imbrseq12((s_mseq1 a tbl num lst),b,
(s_imbr1 c tbl num lst))
| s_imbr1 (Imbrseq13(a,b,c)) tbl num lst
= Imbrseq13((s_imbr1 a tbl num lst),b,
(s_mseq1 c tbl num lst))*)
(* normal form ==> ( i = ini+(j-1)*inc ) *)
and norform(pos1,tbl,name,pos2)
= Plus(Iexpr1(Integer(getini(name,tbl,pos1))),
Iexpr4(Mult(Iexpr4(Plus(Iexpr2(Rangevariable
(Name(stringofint(p12(pos1,pos2))))),
Iexpr4(Iexpr1(Integer ~1)))),
Iexpr1(Integer(getinc(name,tbl,pos1))))))
and p12(p1,p2) = if p1 = p2 then p1 else p2
and getini(name,a::x,pos)
= if name = (#name a) then getini1(pos,(#value a))
else getini(name,x,pos)
| getini(name,[],pos) = error "Impossible"
and getini1(pos,a::x)
= if pos = (#pos a) then (#lower a) else getini1(pos,x)
| getini1(pos,[]) = error "Impossible"
and getinc(name,a::x,pos)
= if name = (#name a) then getinc1(pos,(#value a))
else getinc(name,x,pos)
| getinc(name,[],pos) = error "Impossible"
and getinc1(pos,a::x)
= if pos = (#pos a) then (#step a) else getinc1(pos,x)
| getinc1(pos,[]) = error "Impossible"
and na (Name(a)) = Name a
and na1 (Name(a)) = a
and chkmem(name,a::x)
= if name = (#name a) then true else chkmem(name,x)
| chkmem(name,[]) = false
and mbody(Name(a),tbl,lst,num) = mbody1(a,tbl,tbl,lst,num)
and mbody1(a,(b:Arraytable)::x,tbl,lst,num)
= if a = (#name b) then mbody2(a,(#dim b),1,tbl,lst,num)
else mbody1(a,x,tbl,lst,num)
| mbody1(a,[],tbl,lst,num) = error "Error"
and mbody2(name,dim,i,tbl,lst,num)
= if i = dim
then Meventbody1(norform(i,tbl,name,(chkd(i,num,lst,lst))))
else Meventbody3(norform(i,tbl,name,(chkd(i,num,lst,lst))),
mbody2(name,dim,i+1,tbl,lst,num-1))
and chkd(i,num,a::x,lst)
= if chk(num,(#pos a)) then chkd1(i,(#pos a),num,lst,[])
else chkd(i,num,x,lst)
| chkd(i,num,[],lst) = error "Impossible"
and chkd1(i,a::x,num,lst,l)
= if i = (#d a) then (#p a)
else chkd1(i,x,num,lst,(l@[(#d a)]))
| chkd1(i,[],num,lst,l) = if (member l num)
then i else num
(* create a table that stores the information of distributors *)
and mgel1 (Gelement1(a)) tbl l ct1 = mstel1 a tbl l ct1
| mgel1 (Gelement2(a)) tbl l ct1 = srepl1 a tbl l ct1
| mgel1 (Gelement3(a)) tbl l ct1 = distlst a tbl l ct1
| mgel1 (Gelement4(a,b)) tbl l ct1
= (rrepl1 a tbl l ct1) @ (mgel1 b tbl l ct1)
| mgel1 (Gelement5(a,b)) tbl l ct1
= (mstel1 a tbl l ct1) @ (mgelL1 b tbl l ct1)
| mgel1 (Gelement5_1(a,b)) tbl l ct1
= (srepl1 a tbl l ct1) @ (mgelL1 b tbl l ct1)
| mgel1 (Gelement5_2(a,b)) tbl l ct1
= (distlst a tbl l ct1) @ (mgelL1 b tbl l ct1)
and mgelL1 (GelementL1(a)) tbl l ct1 = lrepl1 a tbl l ct1
| mgelL1 (GelementL2(a,b)) tbl l ct1
= (lrepl1 a tbl l ct1) @ (mgelL1 b tbl l ct1)
and srepl1 (Sreplicator1(a,b)) tbl l ct1 = conc1 b tbl l ct1
| srepl1 (Sreplicator2(a,b)) tbl l ct1 = imbr1 b tbl l ct1
and rrepl1 (Rreplicator1(a,b,c)) tbl l ct1 = conc1 b tbl l ct1
| rrepl1 (Rreplicator2(a,b,c)) tbl l ct1 = imbr1 b tbl l ct1
and lrepl1 (Lreplicator1(a,b,c)) tbl l ct1 = conc1 c tbl l ct1
| lrepl1 (Lreplicator2(a,b,c)) tbl l ct1 = imbr1 c tbl l ct1
and conc1 (Concseq(a,b)) tbl l ct1 = mseq1 a tbl l ct1
and imbr1 (Imbrseq1(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq2(a,b,c,d,e,f,g)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
@ (mseq1 g tbl l ct1)
| imbr1 (Imbrseq3(a,b)) tbl l ct1 = mseq1 b tbl l ct1
| imbr1 (Imbrseq3s(a,b)) tbl l ct1 = mseq1 b tbl l ct1
| imbr1 (Imbrseq4(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq4s(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq5(a,b)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq5s(a,b)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq6(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq6s(a,b,c,d)) tbl l ct1
= (mseq1 a tbl l ct1) @ (mseq1 d tbl l ct1)
| imbr1 (Imbrseq7(a)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq7s(a)) tbl l ct1 = mseq1 a tbl l ct1
| imbr1 (Imbrseq8(a)) tbl l ct1 = imbr1 a tbl l ct1
| imbr1 (Imbrseq8s(a)) tbl l ct1 = imbr1 a tbl l ct1
(*| imbr1 (Imbrseq9(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq9s(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq10(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq10s(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)
| imbr1 (Imbrseq11(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq11s(a,b,c,d,e)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
@ (mseq1 e tbl l ct1)
| imbr1 (Imbrseq12(a,b,c)) tbl l ct1
= (mseq1 a tbl l ct1) @ (imbr1 c tbl l ct1)
| imbr1 (Imbrseq13(a,b,c)) tbl l ct1
= (imbr1 a tbl l ct1) @ (mseq1 c tbl l ct1)*)
and distlst (Distributor1(a,b,c,d)) tbl l ct1
= mseq1 d tbl (l @ [{p=ct1+1, d=iex1 b}]) (ct1+1)
| distlst (Distributor2(a,b,c)) tbl l ct1
= mseq1 c tbl (l @ [{p=ct1+1, d=iex1 b}]) (ct1+1)
| distlst (Distributor3(a,b,c)) tbl l ct1
= mseq1 c tbl (l @ [{p=ct1+1, d=0}]) (ct1+1)
| distlst (Distributor4(a,b)) tbl l ct1
= mseq1 b tbl (l @ [{p=ct1+1,d=0}]) (ct1+1)
and mseq1 (Sequence1(a)) tbl l ct1 = morel1 a tbl l ct1
| mseq1 (Sequence2(a,b)) tbl l ct1
= (morel1 a tbl l ct1) @ (mseq1 b tbl l ct1)
and morel1 (Orelement1(a)) tbl l ct1 = mgel1 a tbl l ct1
| morel1 (Orelement2(a,b)) tbl l ct1
= (mgel1 a tbl l ct1) @ (morel1 b tbl l ct1)
and mstel1 (Nostar(a)) tbl l ct1 = mel1 a tbl l ct1
| mstel1 (Star(a)) tbl l ct1 = mel1 a tbl l ct1
and mel1 (Element(a)) tbl l ct1 = ev a tbl l ct1
| mel1 (Group(a)) tbl l ct1 = mseq1 a tbl l ct1
and ev (Event1(Name a)) tbl l ct1
= [{name=a, dim=getlist22(a,tbl), pos=l}]
| ev (Event2(Name a)) tbl l ct1
= if mem(tbl,a)
then [{name=a, dim=getlist22(a,tbl), pos=l}]
else [] (* if it is not an array (a simple event) *)
| ev (Event3(Name a,b)) tbl l ct1
= if mem (tbl,a)
then [{name=a,dim=(mevbody b 0), pos=l}]
else error "not an array"
and mevbody (Empty) ct = [ct+2] @ [ct+1]
| mevbody (Meventbody1(a)) ct = []
| mevbody (Meventbody2(a)) ct = (mevbody a (ct+1)) @ [ct+1]
| mevbody (Meventbody3(a,b)) ct = mevbody b (ct+1)
| mevbody (Meventbody4(a)) ct = [ct+2]
and getlist22(nname,((a:Arraytable)::x))
= if nname = (#name a) then count1(1,(#dim a))
else getlist22(nname,x)
| getlist22(nname,[]) = []
and count1(ini,fi)
= if ini <= fi
then (count1((ini+1),fi)) @ [ini]
else []
and mem (a::x,y)
= if (y = (#name a)) then true
else mem (x,y)
| mem ([],y) = false
in
fun transform x = trans x
end
end
(* end of file `transform.sml' *)
(* File name: pfirst.sml
Objective: Put all the paths in front of the process.
Input : mprogram
Output : mprogram *)
functor Pfirst(structure CSY: COSY
structure PRLD: PRELUDE): PFIRST =
struct
structure CSY = CSY
val chg=ref 0
local
open CSY
fun pf1 (Program(a)) (chg) = Program(pf_mpb a chg)
and pf_mpb (Programbody1(a)) chg = Programbody1(a)
| pf_mpb (Programbody2(a)) chg = Programbody2(a)
| pf_mpb (Programbody3(a)) chg = Programbody3(a)
| pf_mpb (Programbody4(a,b)) chg
= Programbody4(a,(pf_mpb b chg))
| pf_mpb (Programbody5(a,b)) chg
= Programbody5(a,(pf_mpb b chg))
| pf_mpb (Programbody6(a,b)) chg = pf_mpa(a,b,chg)
| pf_mpb (Programbody7(a,b)) chg
= Programbody7(a,(pf_mpb b chg))
and pf_mpr1(Process(a)) = Programbody2(Process(a))
and pf_mpa (a,Programbody1(b),chg)
= (chg:=1;(Programbody5(b,(pf_mpr1 a))))
| pf_mpa (a,Programbody5(b,c),chg)
= (chg:=1;(Programbody5(b,Programbody6(a,c))))
| pf_mpa (a,Programbody2(b),chg)
= Programbody6(a,Programbody2(b))
| pf_mpa (a,Programbody6(b,c),chg)
= Programbody6(a,pf_mpa(b,c,chg))
| pf_mpa (a,Programbody4(b,c),chg)
= (chg:=1;(Programbody4(b,Programbody6(a,c))))
| pf_mpa other = PRLD.error "Error"
in
fun pathfirst x chg
= let val pff = pf1 x chg
in if (!chg) = 1
then (chg:=0; pathfirst pff chg)
else pff
end
end
end
(* end of file `pfirst.sml' *)
(* File name: expand.sml
Objective: Expand the COSY program.
Input : mprogram
Output : string *)
functor Expand(structure CSY: COSY
structure PRLD: PRELUDE
structure CSR_PRLD: CSR_PRELUDE
structure CSR: CSR
sharing CSR.CSY = CSY = CSR_PRLD.CSY): EXPAND =
struct
structure CSY = CSY
structure PRLD = PRLD
structure CSR_PRLD = CSR_PRLD
structure CSR = CSR
type bound = CSR.bound
type Arraytable = CSR.Arraytable
type unbound = CSR.unbound
val unboundlist = ref [{name=" ", value=0}]
local
open CSY
open PRLD
open CSR_PRLD
open CSR
type bound = {pos : int,
lower : int,
upper : int,
step : int}
type Arraytable = {name : string,
dim : int,
value : bound list}
type unbound = {name : string,
value : int}
open Array
open List
type posl = {p : int, d : int}
type temp1 = {name : string, dim : int list, pos : posl list}
type temp2
= {name : string, m : int, pos : int, value : int list}
val ranvalue = ref [{name=" ",value=0}]
(* function 'expc' -- use to expand collectivisor *)
fun expc x = let val mtb = mktbl(x)
in if mtb = [] then () else (print "{\n"; exp1 mtb) end
and exp1((a:Arraytable)::x)
= (print (#name a);
if check((#value a),[])
then
let
val boundlist = (#value a)
val ini1_ar = array((#dim a),1)
val ini_ar = array((#dim a),1)
val fi_ar=array((#dim a),1)
val inc_ar=array((#dim a),1)
in pr_ar(getini(ini1_ar,(#value a),0),
getini(ini_ar,(#value a),0),
getfi(fi_ar,(#value a),0),
getinc(inc_ar,(#value a),0),(#dim a))
end
else let
val boundlist = (#value a)
in pnt(pr_list(boundlist,[],[],1)) end;
exp1 x)
| exp1 [] = (print"}\n";())
and check(a::x,l) = if member l (#pos a) then false
else check(x,l @ [(#pos a)])
| check([],l) = true
and getfi(fi_ar,(b::y),num)
= if (#pos b) = num+1
then (update(fi_ar,num,(#upper b));
getfi(fi_ar,y,(num+1)))
else getfi(fi_ar,y,num)
| getfi(fi_ar,[],num) = fi_ar
and getini(ini_ar,(b::y),num)
= if (#pos b) = num+1
then (update(ini_ar,num,(#lower b));
getini(ini_ar,y,(num+1)))
else getini(ini_ar,y,num)
| getini(ini_ar,[],num) = ini_ar
and getinc(inc_ar,(b::y),num)
= if (#pos b) = num+1
then (update(inc_ar,num,(#step b));
getinc(inc_ar,y,(num+1)))
else getinc(inc_ar,y,num)
| getinc(inc_ar,[],num) = inc_ar
and pr_ar(ini1_ar,ini_ar,fi_ar,inc_ar,dim)
= if (sub(ini_ar,dim-1)>sub(fi_ar,dim-1))
then print"\n"
else if sub(ini_ar,0) <= sub(fi_ar,0)
then (print (" ("^pr1(ini_ar,dim,0)^")");
pr_ar(ini1_ar,upd(ini_ar,0,
(sub(ini_ar,0)+sub(inc_ar,0))),
fi_ar,inc_ar,dim))
else pr_ar(ini1_ar,pr2(ini1_ar,ini_ar,
fi_ar,inc_ar,dim,0),
fi_ar,inc_ar,dim)
and pr1(ini_ar,dim,num)
= if num < dim
then stringofint(sub(ini_ar,num))^comma(num,dim)
^pr1(ini_ar,dim,num+1)
else ""
and comma(num,dim) = if num = dim-1 then "" else ","
and pr2(ini1_ar,ini_ar,fi_ar,inc_ar,dim,num)
= if dim=num+1 andalso sub(ini_ar,num)>=sub(fi_ar,num)
then upd(ini_ar,num,(sub(ini_ar,num)+sub(inc_ar,num)))
else if (sub(ini_ar,num) >= sub(fi_ar,num))
then pr2(ini1_ar,upd(ini_ar,num,sub(ini1_ar,num)),
fi_ar,inc_ar,dim,(num+1))
else upd(ini_ar,num,(sub(ini_ar,num)+sub(inc_ar,num)))
and upd(ini_ar,num,v) = (update(ini_ar,num,v);ini_ar)
and pr_list(a::x,l,l1,num)
= if num = (#pos a)
then pr_list(x,(l @ [mklist((#lower a),
(#upper a),(#step a))]), l1,num)
else pr_list(x,[mklist((#lower a),
(#upper a),(#step a))], (l1 @ [l]),num+1)
| pr_list([],l,l1,num) = l1 @ [l]
and mklist(ini:int,fi,inc)
= if ini <= fi andalso inc > 0
then [ini] @ mklist(ini+inc,fi,inc)
else if ini >= fi andalso inc < 0
then [ini] @ mklist(ini+inc,fi,inc)
else []
and pnt(a::x) = if (length a) = 1
then pnt1(hd a,hd x)
else pnt2(a,hd(hd x))
| pnt([]) = error "imposible"
and pnt1(a::x,b::y) = (pnt11(a,b);pnt1(x,y))
| pnt1([],[]) = print "\n"
| pnt1([],y) = error "imposible"
| pnt1(x,[]) = error "imposible"
and pnt11(a,b::y)
= (print (" ("^stringofint(a)^","
^stringofint(b)^")");pnt11(a,y))
| pnt11(a,[]) = print ""
and pnt2(a::x,b::y) = (pnt22(a,b);pnt2(x,y))
| pnt2([],[]) = print "\n"
| pnt2([],y) = error "imposible"
| pnt2(x,[]) = error "imposible"
and pnt22(a::x,b)
= (print (" ("^stringofint(a)^","
^stringofint(b)^")");pnt22(x,b))
| pnt22([],b) = print ""
and ex (Program(a))
= "program "^(ex_mpb a (mktbl (Program(a))))^
"endprogram"
and ex_mpb (Programbody1(a)) tbl = ex_mpa a tbl
| ex_mpb (Programbody2(a)) tbl = ex_mpr a tbl
| ex_mpb (Programbody3(a)) tbl = ex_brep a tbl
| ex_mpb (Programbody4(a,b)) tbl = ex_mpb b tbl
| ex_mpb (Programbody5(a,b)) tbl
= (ex_mpa a tbl)^(ex_mpb b tbl)
| ex_mpb (Programbody6(a,b)) tbl
= (ex_mpr a tbl)^(ex_mpb b tbl)
| ex_mpb (Programbody7(a,b)) tbl
= (ex_brep a tbl)^(ex_mpb b tbl)
and ex_mpa (Path(a)) tbl
= "path " ^ lstrip(ex_mseq a tbl) ^ " end "
and ex_mpr (Process(a)) tbl
= "process " ^ (ex_mseq a tbl) ^ " end "
and ex_brep (Bodyreplicator(a,b)) tbl
= n_exprepl(ivar(a),ini(a),fi(a),inc(a),b,1,tbl)
and bbrep (BBodyreplicator1(a)) tbl = ex_mpa a tbl
| bbrep (BBodyreplicator2(a)) tbl = ex_mpr a tbl
| bbrep (BBodyreplicator3(a)) tbl = ex_brep a tbl
| bbrep (BBodyreplicator4(a,b)) tbl
= (ex_mpa a tbl)^(bbrep b tbl)
| bbrep (BBodyreplicator5(a,b)) tbl
= (ex_mpr a tbl)^(bbrep b tbl)
| bbrep (BBodyreplicator6(a,b)) tbl
= (ex_brep a tbl)^(bbrep b tbl)
and ex_mseq (Sequence1(a)) tbl = ex_mor a tbl
| ex_mseq (Sequence2(a,b)) tbl
= (ex_mor a tbl)^";"^(ex_mseq b tbl)
and ex_mor (Orelement1(a)) tbl = ex_gel a tbl
| ex_mor (Orelement2(a,b)) tbl
= (ex_gel a tbl)^","^(ex_mor b tbl)
and ex_gel (Gelement1(a)) tbl = ex_mstel a tbl
| ex_gel (Gelement2(a)) tbl = srepl a tbl
| ex_gel (Gelement3(a)) tbl = ""
| ex_gel (Gelement4(a,b)) tbl
= (ex_gel b tbl)^(rrepl a tbl)
| ex_gel (Gelement5(a,b)) tbl
= (ex_mstel a tbl)^(ex_gelL b tbl)
| ex_gel (Gelement5_1(a,b)) tbl
= (srepl a tbl)^(ex_gelL b tbl)
| ex_gel (Gelement5_2(a,b)) tbl = ""
and ex_gelL (GelementL1(a)) tbl = lrepl a tbl
| ex_gelL (GelementL2(a,b)) tbl
= (lrepl a tbl)^(ex_gelL b tbl)
and ex_mel (Element(a)) tbl = ex_mev a
| ex_mel (Group(a)) tbl = "("^(ex_mseq a tbl)^")"
and ex_mstel (Nostar(a)) tbl = ex_mel a tbl
| ex_mstel (Star(a)) tbl = (ex_mel a tbl)^"*"
and ex_mev (Event2(a)) = (na a)
| ex_mev (Event3(a,b)) = (na a) ^ "(" ^ (evb b) ^ ")"
| ex_mev other = ""
and evb (Meventbody1(a)) = stringofint(ival(a))
| evb (Meventbody3(a,b)) = stringofint(ival(a))^","^(evb b)
| evb other = ""
and conc (Concseq(a,b)) tbl ran1
= lstrip(n_exprepl1(ivar(ran1),ini(ran1),
fi(ran1),inc(ran1), a,1,tbl,(seper(b))))
and seper(Comma(a)) = a
| seper(Simicol(a)) = a
and srepl (Sreplicator1(a,b)) tbl = conc b tbl a
| srepl (Sreplicator2(a,b)) tbl = imbr b tbl a "" ""
and imbr (Imbrseq1(a,b,c,d,e)) tbl ran1 left right
= lstrip(n_exprepl2(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),a,1,tbl,(seper(b)),left))
^(seper(c))
^fstrip(n_exprepl4(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),e,1,tbl,(seper(d)),right))
| imbr (Imbrseq2(a,b,c,d,e,f,g)) tbl ran1 left right
= lstrip(n_exprepl2(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),a,1,tbl,(seper(b)),left))
^(seper(c))^(ex_mseq d tbl)^(seper(e))
^fstrip(n_exprepl4(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),g,1,tbl,(seper(f)),right))
| imbr (Imbrseq3(a,b)) tbl ran1 left right
= n_exprepl5(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,"(")
^fstrip(n_exprepl4(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),b,1,tbl,(seper(a)),")"))
| imbr (Imbrseq3s(a,b)) tbl ran1 left right
= n_exprepl5(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,"(")
^fstrip(n_exprepl4(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1), b,1,tbl,(seper(a)),")*"))
| imbr (Imbrseq4(a,b,c,d)) tbl ran1 left right
= n_exprepl5(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,"(")^(ex_mseq a tbl)^(seper(b))
^fstrip(n_exprepl4(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),d,1,tbl,(seper(c)),")"))
| imbr (Imbrseq4s(a,b,c,d)) tbl ran1 left right
= n_exprepl5(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,"(")
^(ex_mseq a tbl)^(seper(b))
^fstrip(n_exprepl4(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1), d,1,tbl,(seper(c)),")*"))
| imbr (Imbrseq5(a,b)) tbl ran1 left right
= lstrip(n_exprepl2(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1), a,1,tbl,(seper(b)),"("))
^n_exprepl6(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,")")
| imbr (Imbrseq5s(a,b)) tbl ran1 left right
= lstrip(n_exprepl2(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1), a,1,tbl,(seper(b)),"("))
^n_exprepl6(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,")*")
| imbr (Imbrseq6(a,b,c,d)) tbl ran1 left right
= lstrip(n_exprepl2(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1), a,1,tbl,(seper(b)),"("))
^(seper(c))^(ex_mseq d tbl)
^n_exprepl6(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,")")
| imbr (Imbrseq6s(a,b,c,d)) tbl ran1 left right
= lstrip(n_exprepl2(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1), a,1,tbl,(seper(b)),"("))
^(seper(c))^(ex_mseq d tbl)
^n_exprepl6(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,")*")
| imbr (Imbrseq7(a)) tbl ran1 left right
= n_exprepl5(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,"(")
^(ex_mseq a tbl)
^n_exprepl6(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,")")
| imbr (Imbrseq7s(a)) tbl ran1 left right
= n_exprepl5(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,"(")
^(ex_mseq a tbl)
^n_exprepl6(ivar(ran1),ini(ran1),fi(ran1),
inc(ran1),1,")*")
| imbr (Imbrseq8(a)) tbl ran1 left right
= imbr a tbl ran1 "(" ")"
| imbr (Imbrseq8s(a)) tbl ran1 left right
= imbr a tbl ran1 "(" ")*"
(*| imbr (Imbrseq9(a,b,c)) tbl
= (ex_mseq a tbl);(imbr c tbl)
| imbr (Imbrseq9s(a,b,c)) tbl
= (ex_mseq a tbl);(imbr c tbl)
| imbr (Imbrseq10(a,b,c)) tbl
= (imbr a tbl);(ex_mseq c tbl)
| imbr (Imbrseq10s(a,b,c)) tbl
= (imbr a tbl);(ex_mseq c tbl)
| imbr (Imbrseq11(a,b,c,d,e)) tbl
= (ex_mseq a tbl);(imbr c tbl);(ex_mseq e tbl)
| imbr (Imbrseq11s(a,b,c,d,e)) tbl
= (ex_mseq a tbl);(imbr c tbl);(ex_mseq e tbl)
| imbr (Imbrseq12(a,b,c)) tbl
= (ex_mseq a tbl);(imbr c tbl)
| imbr (Imbrseq13(a,b,c)) tbl
= (imbr a tbl);(ex_mseq c tbl)*)
and rrepl (Rreplicator1(a,b,c)) tbl
= (conc b tbl a)^(seper(c))
| rrepl (Rreplicator2(a,b,c)) tbl
= (imbr b tbl a "" "")^(seper(c))
and lrepl (Lreplicator1(a,b,c)) tbl
= (seper(b))^(conc c tbl a)
| lrepl (Lreplicator2(a,b,c)) tbl
= (seper(b))^(imbr c tbl a "" "")
and na (Name(a)) = a
and ivar(Range_spec(Indexvariable(Name a),b,c,d)) = a
and ini(Range_spec(a,b,c,d)) = iex b
and fi(Range_spec(a,b,c,d)) = iex c
and inc(Range_spec(a,b,c,d)) = iex d
and ival (Iexpr1(Integer a)) = a
| ival (Iexpr2(Rangevariable(Name a)))
= if checkvalue(a,(!unboundlist))
then getv(a,(!unboundlist))
else getv1(a,(!ranvalue))
| ival (Plus(a,b)) = ival(a) + ival(b)
| ival (Mult(a,b)) = ival(a) * ival(b)
| ival (Div(a,b)) = ival(a) div ival(b)
| ival (Pow(a,b)) = power(ival(a),ival(b))
| ival (Iexpr4(a)) = ival(a)
| ival (other) = error "imposible"
and checkvalue(a,((l:unbound)::x))
= if a = (#name l) then true else checkvalue(a,x)
| checkvalue(a,[]) = false
and getv(a,((l:unbound)::x))
= if a = (#name l) then (#value l) else getv(a,x)
| getv(a,[]) = error "iiiImpossible" handle Error => 0
and getv1(a,((l:unbound)::x))
= if a = (#name l) then (#value l) else getv1(a,x)
| getv1(a,[]) = error "Impossible" handle Error => 0
and lstrip(x) = let val ss = substring(x,(size(x)-1),1)
in if ss = ";" orelse ss =","
then substring(x,0,(size(x)-1))
else x
end
and fstrip(x) = let val ss = substring(x,0,1)
in if ss = ";" orelse ss =","
then substring(x,1,(size(x)-1))
else x
end
and n_exprepl(ivr,ini,fi,inc,spqbr,j,tbl)
= let val m = (fi-ini) div inc + 1
val i=ini+(j-1)*inc
in ranvalue := as_value(ivr,(!ranvalue),i,[]);
if j<=m then (bbrep spqbr tbl)
^ n_exprepl(ivr,ini,fi,inc,spqbr,j+1,tbl)
else ""
end
and as_value(ivr,((l:unbound)::x),i,ranlst)
= if ivr = (#name l)
then ranlst @ [{name=ivr,value=i}] @ x
else as_value(ivr,x,i,(ranlst @ [l]))
| as_value(ivr,[],i,ranlst) = ranlst @ [{name=ivr,value=i}]
and n_exprepl1(ivr,ini,fi,inc,mseq,j,tbl,sep1)
= let val m = (fi-ini) div inc + 1
val i=ini+(j-1)*inc
in ranvalue := as_value(ivr,(!ranvalue),i,[]);
if j<=m then (ex_mseq mseq tbl)^sep1
^n_exprepl1(ivr,ini,fi,inc,mseq,j+1,tbl,sep1)
else ""
end
(* for the 'p' in #i:1,3,1[p@t@q] *)
and n_exprepl2(ivr,ini,fi,inc,mseq,j,tbl,sep1,left)
= let val m = (fi-ini) div inc + 1
val i=ini+(j-1)*inc
in ranvalue := as_value(ivr,(!ranvalue),i,[]);
if j<=m then left^(ex_mseq mseq tbl)^sep1
^n_exprepl2(ivr,ini,fi,inc,mseq,j+1,tbl,sep1,left)
else ""
end
(* for the 'q' in #i:1,3,1[p@t@q] *)
and n_exprepl4(ivr,ini,fi,inc,mseq,j,tbl,sep1,right)
= let val m = (fi-ini) div inc + 1
in (if inc > 0 then
ranvalue := as_value(ivr,(!ranvalue),
(m-(j-1)*inc),[])
else ranvalue := as_value(ivr,(!ranvalue),
(m-(j-m)*inc),[]));
if j<=m then sep1^(ex_mseq mseq tbl)^right
^n_exprepl4(ivr,ini,fi,inc,mseq,j+1,tbl,sep1,right)
else ""
end
(* for those without 'p' in #i:1,3,1[p@t@q] *)
and n_exprepl5(ivr,ini,fi,inc,j,left)
= let val m = (fi-ini) div inc + 1
in if j<=m then left^n_exprepl5(ivr,ini,fi,inc,j+1,left)
else ""
end
(* for those without 'q' in #i:1,3,1[p@t@q] *)
and n_exprepl6(ivr,ini,fi,inc,j,right)
= let val m = (fi-ini) div inc + 1
in if j<=m then n_exprepl6(ivr,ini,fi,inc,j+1,right)^right
else ""
end
in
fun expand x = (expc x;ex x)
end;
end
(* end of file `expand.sml' *)
(* File name: cosyenv.sml
Objective: This file combines the syntactic analyzer, context
-sensitive restriction checker and expander.
While running this program, it does syntactic analysis.
Then, It checks all constext-sensitive restriction.
Then, it does expansion.
Input : string
Output : string *)
functor Cosyenv(structure CSY: COSY
structure LX: LEX
structure PRLD: PRELUDE
structure PRSR_BLDR: PARSER_BUILDER
structure PRSR: PARSER
structure CSR_PRLD: CSR_PRELUDE
structure CSR: CSR
structure PFRST: PFIRST
structure TRNSFRM: TRANSFORM
structure XPND: EXPAND
sharing PRSR.CSY = XPND.CSY = TRNSFRM.CSY
= CSR_PRLD.CSY = PFRST.CSY = CSR.CSY = CSY
and CSR_PRLD.LX = PRSR_BLDR.LX = PRSR.LX = LX
and PRSR.PRSR_BLDR = PRSR_BLDR): COSYENV =
struct
structure CSY = CSY
structure LX = LX
structure PRLD = PRLD
structure PRSR_BLDR = PRSR_BLDR
structure PRSR = PRSR
structure CSR_PRLD = CSR_PRLD
structure CSR = CSR
structure PFRST = PFRST
structure TRNSFRM = TRNSFRM
structure XPND = XPND
local
open CSY
open LX
open PRLD
open PRSR_BLDR
open PRSR
open CSR_PRLD
open CSR
open PFRST
open XPND
open TRNSFRM
fun p_c_e x = let val lex_token = lex x
in if !err_lex <> 0
then error ((stringofint (!err_lex)) ^
" lexical error(s) found !!!") handle Error =>""
else let val mp_parser = m_parser lex_token
in if report(mp_parser) then (csr (report1(mp_parser)))
else error "Parse error(s) found !!!" handle Error => ""
end
end
and lex x = let
in err_lex := 0; lexanal(explode x) end
and report (Ok (c,[])) = true
| report other = false
and report1 (Ok (c,[])) = c
| report1 other = error "Impossible"
and csr x = let val unbl = [{name=" ",value=0}]
in err_cnt := 0;
unboundlist := unbl;
chg := 0;
crest1 x; (* check Crest1 : upperbound < lowerbound *)
crest2 x; (* check Crest2 : duplicate array name *)
crest3 x; (* check Crest3 : the range is empty *)
irest1 x; (* check Irest1 : index and range use the same
name*)
irest2 x; (* check Irest2 : use index outside the []*)
brrest x; (* check BRrest : the range of bodyreplicator
is empty *)
rrest11 x; (* check Rrest1.1 : inc = 0 *)
rrest12 x; (* check Rrest1.2 : (fi-in) div inc+1 <= 0 *)
rrest13 x; (* check Rrest1.3 : (fi-in) div inc+1 <=0 and
FSTRIP(LSTRIP(t)) = *)
rrest2 x; (* check Rrest2 : range is out of boundary *)
drest1 x; (* check Drest1 : no slice event in distributor *)
drest21 x; (* check Drest2.1 :do not have the same sections*)
drest22 x; (* check Drest2.2 : do not have the same sections
at jth dimension *)
drest3 x; (* check Drest3 : more or less than the number of
distributable dimensions *)
drest4 x; (* check Drest4 : jth dimension is not a
distributable dimension *)
drest5152 x; (* check Drest5.1 and Drest5.2 :
i1,i2,i3 have problems *)
if !err_cnt = 0
then (print "No errrs !!! \n";
expand(transform (pathfirst x chg)))
else (print (stringofint(!err_cnt) ^
" error(s) found !!! \n");"")
end
in fun parser_csr_expand x = p_c_e x
end
(* displayer *)
local
val print = String.print;
fun disp x
= let val si = size(x)
in if (si < 80) then print (x^"\n\n")
else pr1(x,0,0,0,"",si) end
and pr1(x,i,pos,num,temp,si)
= let val char = substring(x,i,1)
in if char = " " then
(if temp = "program"
then (print(temp^"\n");pr1(x,i+1,i+1,0,"",si))
else if temp = "path" orelse temp = "process" then
pr2(x,temp^char,i+1,num+1,"")
else print temp)
else if (i+1 = si) then print (temp^"m\n\n")
else (pr1(x,i+1,pos,num+1,temp^char,si))
end
and pr2(x,temp,i,num,temp1)
= let val char = substring(x,i,1)
in if char = " " then
(if temp1 = "end"
then (if num < 80 then (print (" "^temp^temp1^"\n");
pr1(x,i+1,i+1,0,"",size(x)))
else (pr3(temp^temp1,0,size(temp^temp1),"","");
pr1(x,i+1,i+1,0,"",size(x))))
else (pr2(x,temp^temp1^char,i+1,num+1,"")))
else (pr2(x,temp,i+1,num+1,temp1^char))
end
and pr3(temp,i,si,temp1,temp2)
= let val char = substring(temp,i,1)
in if char = " " then
(if temp1 = "path" orelse temp1 = "process" then
(print (" "^temp1^"\n ");
pr3(temp,i+1,si,"",""))
else print (temp1^"\n end\n"))
else if char = "," then
(if (ord(temp2)<58 andalso ord(temp2)>47) andalso
(ord(substring(temp,i+1,1))<58 andalso
ord(substring(temp,i+1,1))>47)
then pr3(temp,i+1,si,temp1^char,char)
else (print (temp1^"\n ,");
pr3(temp,i+1,si,"","")))
else if char = ";" then
(print (temp1^"\n ;");
pr3(temp,i+1,si,"",""))
else pr3(temp,i+1,si,temp1^char,char)
end
in
fun display x = disp x
end
end
(* end of file `cosyenv.sml' *)
(* File name: build.sml
Objective: Compile and open the system to implement a new Macro
COSY environment *)
(* load all signatures and functors *)
use "prelude.sig";
use "prelude.sml";
use "cosy.sig";
use "cosy.sml";
use "nmp_lex.sig";
use "nmp_lex.sml";
use "parser_prelude.sig";
use "parser_prelude.sml";
use "nmp_parser.sig";
use "nmp_parser.sml";
use "csr_prelude.sig";
use "csr_prelude.sml";
use "csr.sig";
use "csr.sml";
use "transform.sig";
use "transform.sml";
use "pfirst.sig";
use "pfirst.sml";
use "expand.sig";
use "expand.sml";
use "cosyenv.sig";
use "cosyenv.sml";
(* declare structures *)
structure Prld = Prelude();
structure Csy = Cosy();
structure Lx = Lex(structure PRLD = Prld);
structure Prsr_bldr = Parser_builder(structure LX = Lx);
structure Prsr = Parser(structure PRLD = Prld
structure PRSR_BLDR = Prsr_bldr
structure CSY = Csy
structure LX = Lx);
structure Csr_prld = Csr_prelude(structure CSY = Csy
structure LX = Lx
structure PRLD = Prld);
structure Csr = Csr(structure CSY = Csy
structure CSR_PRLD = Csr_prld
structure PRLD = Prld);
structure Trnsfrm = Transform(structure CSY = Csy
structure PRLD = Prld
structure CSR_PRLD = Csr_prld
structure CSR = Csr);
structure Pfrst = Pfirst(structure CSY = Csy
structure PRLD = Prld);
structure Xpnd = Expand(structure CSY = Csy
structure PRLD = Prld
structure CSR_PRLD = Csr_prld
structure CSR = Csr);
structure Csynv = Cosyenv(structure CSY = Csy
structure LX = Lx
structure PRLD = Prld
structure PRSR_BLDR = Prsr_bldr
structure PRSR = Prsr
structure CSR_PRLD = Csr_prld
structure CSR = Csr
structure PFRST = Pfrst
structure TRNSFRM = Trnsfrm
structure XPND = Xpnd);
(* open the system *)
open Prld;
open Csynv;
(* end of file `build.sml' *)