(* $Id: clkexprtrans.sml 49 2008-07-21 07:02:40Z tbourke $ *)
|
(* $Id: clkexprtrans.sml 62 2008-08-20 11:20:33Z tbourke $
|
|
*
|
|
* Copyright (c) 2008 Timothy Bourke (University of NSW and NICTA)
|
|
* All rights reserved.
|
|
*
|
|
* This program is free software; you can redistribute it and/or modify it
|
|
* under the terms of the "BSD License" which is distributed with the
|
|
* software in the file LICENSE.
|
|
*
|
|
* This program is distributed in the hope that it will be useful, but
|
|
* WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the BSD
|
|
* License for more details.
|
|
*)
|
|
|
(* TODO:
|
(* TODO:
|
* - rename `paritition' to `constraint'
|
* - rename `paritition' to `constraint'
|
* more generally it is used to constrain the applicability of
|
* more generally it is used to constrain the applicability of
|
* a set of transitions and is not affected by negation.
|
* a set of transitions and is not affected by negation.
|
*)
|
*)
|
|
|
structure ClkExprTrans :> CLK_EXPR_TRANS = let
|
structure ClkExprTrans :> CLK_EXPR_TRANS = let
|
structure E = Expression
|
structure E = Expression
|
and ClkE = ClockExpression
|
and ClkE = ClockExpression
|
and AT = ActionTrans
|
and AT = ActionTrans
|
and ST = SelTrans
|
and ST = SelTrans
|
and Env = Environment
|
and Env = Environment
|
and ECVT = ExpressionCvt
|
and ECVT = ExpressionCvt
|
in struct
|
in struct
|
|
|
type expr = Expression.expr
|
type expr = Expression.expr
|
and ty = Expression.ty
|
and ty = Expression.ty
|
and symbol = Atom.atom
|
and symbol = Atom.atom
|
and symbolset = AtomSet.set
|
and symbolset = AtomSet.set
|
|
|
exception SelectIdConflictsWithForAll of symbol list * symbol list
|
exception SelectIdConflictsWithForAll of symbol list * symbol list
|
|
|
infix <+ <- ++ <\ \ =:= ; open Symbol
|
infix <+ <- ++ <\ \ =:= ; open Symbol
|
|
|
(* Invariants:
|
(* Invariants:
|
- names contains all free names and those bound by select and forall
|
- names contains all free names and those bound by select and forall
|
- the sets of names of the select and forall lists are disjoint
|
- the sets of names of the select and forall lists are disjoint
|
*)
|
*)
|
datatype t = CETrans of {actselect: (symbol * E.ty) list,(* SelectSub ids *)
|
datatype t = CETrans of {actselect: (symbol * E.ty) list,(* SelectSub ids *)
|
gselect: (symbol * E.ty) list,(* Guard selects *)
|
gselect: (symbol * E.ty) list,(* Guard selects *)
|
forall: (symbol * E.ty) list,(* in prenex form *)
|
forall: (symbol * E.ty) list,(* in prenex form *)
|
partition: Expression.expr,
|
partition: Expression.expr,
|
guard: ClkE.t,
|
guard: ClkE.t,
|
action: ActionTrans.actionsub list,
|
action: ActionTrans.actionsub list,
|
names: symbolset}
|
names: symbolset}
|
|
|
fun addNameTypes xs = let
|
fun addNameTypes xs = let
|
fun add ((n, _), s) = s <+ n
|
fun add ((n, _), s) = s <+ n
|
in foldl add emptyset xs end
|
in foldl add emptyset xs end
|
|
|
local (*{{{1*)
|
local (*{{{1*)
|
fun showCheckedActions [] = ""
|
fun showCheckedActions [] = ""
|
| showCheckedActions (AT.SelectSub s::es) = "[#" ^ Atom.toString s ^ "#]" ^
|
| showCheckedActions (AT.SelectSub s::es) = "[#" ^ Atom.toString s ^ "#]" ^
|
showCheckedActions es
|
showCheckedActions es
|
| showCheckedActions (AT.FreeExprSub e::es) = "[" ^ ECVT.Expr.toString e ^ "]" ^
|
| showCheckedActions (AT.FreeExprSub e::es) = "[" ^ ECVT.Expr.toString e ^ "]" ^
|
showCheckedActions es
|
showCheckedActions es
|
fun symtyToStr (s, ty) = Atom.toString s ^ " : " ^ ECVT.Ty.toString ty
|
fun symtyToStr (s, ty) = Atom.toString s ^ " : " ^ ECVT.Ty.toString ty
|
val symtyList = (ListFormat.fmt {init="(", sep=", ",
|
val symtyList = (ListFormat.fmt {init="(", sep=", ",
|
final=")", fmt=symtyToStr})
|
final=")", fmt=symtyToStr})
|
in (*}}}1*)
|
in (*}}}1*)
|
fun toString (CETrans {actselect, gselect, forall,
|
fun toString (CETrans {actselect, gselect, forall,
|
partition, guard, action, names}) = let
|
partition, guard, action, names}) = let
|
in
|
in
|
"{actselect: " ^ symtyList actselect ^ "\n" ^
|
"{actselect: " ^ symtyList actselect ^ "\n" ^
|
" gselect: " ^ symtyList gselect ^ "\n" ^
|
" gselect: " ^ symtyList gselect ^ "\n" ^
|
" forall: " ^ symtyList forall ^ "\n" ^
|
" forall: " ^ symtyList forall ^ "\n" ^
|
" partition: " ^ ECVT.Expr.toString partition ^ "\n" ^
|
" partition: " ^ ECVT.Expr.toString partition ^ "\n" ^
|
" guard: " ^ ClkE.toString guard ^ "\n" ^
|
" guard: " ^ ClkE.toString guard ^ "\n" ^
|
" action: " ^ showCheckedActions action ^ "\n" ^
|
" action: " ^ showCheckedActions action ^ "\n" ^
|
" names: " ^ AtomSet.foldl
|
" names: " ^ AtomSet.foldl
|
(fn (s, str)=> str ^ " " ^ Atom.toString s) "" names ^
|
(fn (s, str)=> str ^ " " ^ Atom.toString s) "" names ^
|
" }\n"
|
" }\n"
|
end
|
end
|
end (* local *)
|
end (* local *)
|
|
|
fun unionNames cetrans = let
|
fun unionNames cetrans = let
|
fun f (CETrans {names, ...}, m) = m ++ names
|
fun f (CETrans {names, ...}, m) = m ++ names
|
in foldl f emptyset cetrans end
|
in foldl f emptyset cetrans end
|
|
|
fun fromATrans preenv (AT.ActTrans {selectids=sellist,
|
fun fromATrans preenv (AT.ActTrans {selectids=sellist,
|
actionsubs, guard, names}) =
|
actionsubs, guard, names}) =
|
let
|
let
|
val senv = List.foldl (Env.addId Env.SelectScope) preenv sellist
|
val senv = List.foldl (Env.addId Env.SelectScope) preenv sellist
|
val (guard, forall, used) = ClkE.fromExpr (names, senv, guard)
|
val (guard, forall, used) = ClkE.fromExpr (names, senv, guard)
|
(* Note: ClkE.fromExpr ensures:
|
(* Note: ClkE.fromExpr ensures:
|
* intersection(selectids, forall) = emptyset
|
* intersection(selectids, forall) = emptyset
|
* as names includes selectids.
|
* as names includes selectids.
|
*)
|
*)
|
val actionNames = AT.addSelectSubNames actionsubs
|
val actionNames = AT.addSelectSubNames actionsubs
|
|
|
fun categorize ([], acts, gs) = (acts, gs)
|
fun categorize ([], acts, gs) = (acts, gs)
|
| categorize ((s as (n, _))::ss, acts, gs) =
|
| categorize ((s as (n, _))::ss, acts, gs) =
|
if n <- actionNames then categorize (ss, s::acts, gs)
|
if n <- actionNames then categorize (ss, s::acts, gs)
|
else categorize (ss, acts, s::gs)
|
else categorize (ss, acts, s::gs)
|
|
|
val (actsels, gsels) = categorize (sellist, [], [])
|
val (actsels, gsels) = categorize (sellist, [], [])
|
in
|
in
|
CETrans {actselect=actsels,
|
CETrans {actselect=actsels,
|
gselect=gsels,
|
gselect=gsels,
|
forall=forall,
|
forall=forall,
|
partition=E.trueExpr,
|
partition=E.trueExpr,
|
guard=guard,
|
guard=guard,
|
action=actionsubs,
|
action=actionsubs,
|
names=used}
|
names=used}
|
end
|
end
|
|
|
fun fromSTrans preenv actsels (ST.SelTrans {selectids, guard, names}) =
|
fun fromSTrans preenv actsels (ST.SelTrans {selectids, guard, names}) =
|
let
|
let
|
val senv = List.foldl (Env.addId Env.SelectScope) preenv actsels
|
val senv = List.foldl (Env.addId Env.SelectScope) preenv actsels
|
val senv' = List.foldl (Env.addId Env.SelectScope) senv selectids
|
val senv' = List.foldl (Env.addId Env.SelectScope) senv selectids
|
val (guard, forall, used) = ClkE.fromExpr (names, senv', guard)
|
val (guard, forall, used) = ClkE.fromExpr (names, senv', guard)
|
(* Note: ClkE.fromExpr ensures:
|
(* Note: ClkE.fromExpr ensures:
|
* intersection(selectids, forall) = emptyset
|
* intersection(selectids, forall) = emptyset
|
* as names includes selectids.
|
* as names includes selectids.
|
*)
|
*)
|
in
|
in
|
CETrans {actselect=actsels,
|
CETrans {actselect=actsels,
|
gselect=selectids,
|
gselect=selectids,
|
forall=forall,
|
forall=forall,
|
partition=E.trueExpr,
|
partition=E.trueExpr,
|
guard=guard,
|
guard=guard,
|
action=map (fn (nm, _)=>AT.SelectSub nm) actsels,
|
action=map (fn (nm, _)=>AT.SelectSub nm) actsels,
|
names=used}
|
names=used}
|
end
|
end
|
|
|
local (**)
|
local (**)
|
fun toBoundId (s, ty) = E.BoundId (s, ty)
|
fun toBoundId (s, ty) = E.BoundId (s, ty)
|
in (**)
|
in (**)
|
fun toTrans (CETrans {actselect, gselect, forall,
|
fun toTrans (CETrans {actselect, gselect, forall,
|
partition, guard, action, ...}) = let
|
partition, guard, action, ...}) = let
|
val preguard = ClkE.toExpr (guard, forall)
|
val preguard = ClkE.toExpr (guard, forall)
|
val guard = if E.equal (partition, E.trueExpr) then preguard
|
val guard = if E.equal (partition, E.trueExpr) then preguard
|
else E.BinBoolExpr {left=partition,bop=E.AndOp,right=preguard}
|
else E.BinBoolExpr {left=partition,bop=E.AndOp,right=preguard}
|
in
|
in
|
{selectids=map toBoundId (actselect @ gselect),
|
{selectids=map toBoundId (actselect @ gselect),
|
actionsubs=map AT.actionsubToExpr action,
|
actionsubs=map AT.actionsubToExpr action,
|
guard=guard}
|
guard=guard}
|
end
|
end
|
end (* local *)
|
end (* local *)
|
|
|
fun rename (CETrans {actselect, gselect, forall, partition,
|
fun rename (CETrans {actselect, gselect, forall, partition,
|
guard, action, names}, r as {old, new}) =
|
guard, action, names}, r as {old, new}) =
|
let
|
let
|
val _ = if new <- names
|
val _ = if new <- names
|
then raise Fail "rename: new name is already bound"
|
then raise Fail "rename: new name is already bound"
|
else ()
|
else ()
|
|
|
fun rsel (sv, sty) = if sv =:= old then (new, sty) else (sv, sty)
|
fun rsel (sv, sty) = if sv =:= old then (new, sty) else (sv, sty)
|
|
|
fun renameAction (a as AT.SelectSub n) = if n =:= old
|
fun renameAction (a as AT.SelectSub n) = if n =:= old
|
then AT.SelectSub new else a
|
then AT.SelectSub new else a
|
| renameAction (AT.FreeExprSub e) = AT.FreeExprSub (E.renameVar (r, e))
|
| renameAction (AT.FreeExprSub e) = AT.FreeExprSub (E.renameVar (r, e))
|
in
|
in
|
CETrans {actselect=map rsel actselect,
|
CETrans {actselect=map rsel actselect,
|
gselect=map rsel gselect,
|
gselect=map rsel gselect,
|
forall=map rsel forall,
|
forall=map rsel forall,
|
partition=E.renameVar (r, partition),
|
partition=E.renameVar (r, partition),
|
guard=ClkE.rename (r, guard),
|
guard=ClkE.rename (r, guard),
|
action=map renameAction action,
|
action=map renameAction action,
|
names=(names <\ old) <+ new}
|
names=(names <\ old) <+ new}
|
end
|
end
|
|
|
local (*{{{1*)
|
local (*{{{1*)
|
fun pairwiseIntersect ([], i) = i
|
fun pairwiseIntersect ([], i) = i
|
| pairwiseIntersect (x::ys, i) = let
|
| pairwiseIntersect (x::ys, i) = let
|
fun withEach (y,i) = AtomSet.union (AtomSet.intersection(x,y), i)
|
fun withEach (y,i) = AtomSet.union (AtomSet.intersection(x,y), i)
|
in pairwiseIntersect (ys, foldl withEach i ys) end
|
in pairwiseIntersect (ys, foldl withEach i ys) end
|
|
|
fun makeTrans cinv_fall
|
fun makeTrans cinv_fall
|
(actselects, potselects, potforalls, part, act)
|
(actselects, potselects, potforalls, part, act)
|
andx =
|
andx =
|
let
|
let
|
fun combineAnd (t, e) = ClkE.And (e, ClkE.Term t)
|
fun combineAnd (t, e) = ClkE.And (e, ClkE.Term t)
|
fun makeAnd [] = ClkE.Term (ClkE.NonClock (E.falseExpr))
|
fun makeAnd [] = ClkE.Term (ClkE.NonClock (E.falseExpr))
|
| makeAnd (x::xs) = List.foldl combineAnd (ClkE.Term x) xs
|
| makeAnd (x::xs) = List.foldl combineAnd (ClkE.Term x) xs
|
|
|
val e=makeAnd andx
|
val e=makeAnd andx
|
val exprNames=ClkE.getFree e
|
val exprNames=ClkE.getFree e
|
val names=exprNames ++ AT.addActionNames act ++ addNameTypes cinv_fall
|
val names=exprNames ++ AT.addActionNames act ++ addNameTypes cinv_fall
|
|
|
val forAlls=List.filter (fn (nm, _)=> nm<-exprNames) potforalls
|
val forAlls=List.filter (fn (nm, _)=> nm<-exprNames) potforalls
|
in
|
in
|
(CETrans {actselect=actselects,
|
(CETrans {actselect=actselects,
|
gselect=List.filter (fn (nm,_)=> nm<-names) potselects,
|
gselect=List.filter (fn (nm,_)=> nm<-names) potselects,
|
forall=forAlls @ cinv_fall,
|
forall=forAlls @ cinv_fall,
|
partition=part,
|
partition=part,
|
guard=e,
|
guard=e,
|
action=act,
|
action=act,
|
names=names},
|
names=names},
|
addNameTypes (forAlls @ cinv_fall))
|
addNameTypes (forAlls @ cinv_fall))
|
end
|
end
|
|
|
in (*}}}1*)
|
in (*}}}1*)
|
fun negate (cinv_fall, cinv)
|
fun negate (cinv_fall, cinv)
|
(cet as CETrans {actselect, gselect, forall, guard,
|
(cet as CETrans {actselect, gselect, forall, guard,
|
partition, action, names}) =
|
partition, action, names}) =
|
let
|
let
|
val g' = ClkE.negate guard
|
val g' = ClkE.negate guard
|
val (e, tnone) = case (ClkE.isConstant g', ClkE.isConstant cinv) of
|
val (e, tnone) = case (ClkE.isConstant g', ClkE.isConstant cinv) of
|
(SOME true, SOME true) => (ClkE.trueExpr, false)
|
(SOME true, SOME true) => (ClkE.trueExpr, false)
|
| (SOME true, _) => (cinv, false)
|
| (SOME true, _) => (cinv, false)
|
| (_, SOME true) => (g', false)
|
| (_, SOME true) => (g', false)
|
| (NONE, NONE) => (ClkE.And (cinv,g'),false)
|
| (NONE, NONE) => (ClkE.And (cinv,g'),false)
|
| _ => (ClkE.falseExpr, true)
|
| _ => (ClkE.falseExpr, true)
|
val dnf = ClkE.toDNF e
|
val dnf = ClkE.toDNF e
|
|
|
val _ = Util.debugVeryDetailed (fn()=>["* CETrans.negate before:\n",
|
val _ = Util.debugVeryDetailed (fn()=>["* CETrans.negate before:\n",
|
toString cet])
|
toString cet])
|
|
|
(* Check the assumption of disjointness: *)
|
(* Check the assumption of disjointness: *)
|
fun addAndCheck ((n, _), s) = if n <- s
|
fun addAndCheck ((n, _), s) = if n <- s
|
then raise Fail "addDisjointForalls"
|
then raise Fail "addDisjointForalls"
|
else s <+ n
|
else s <+ n
|
val _ = foldl addAndCheck (ClkE.getFree g') cinv_fall
|
val _ = foldl addAndCheck (ClkE.getFree g') cinv_fall
|
in
|
in
|
if tnone then [] else (* guard was false *)
|
if tnone then [] else (* guard was false *)
|
if ClkE.conflictExists (addNameTypes gselect, addNameTypes forall, dnf)
|
if ClkE.conflictExists (addNameTypes gselect, addNameTypes forall, dnf)
|
then raise SelectIdConflictsWithForAll (#1 (ListPair.unzip gselect),
|
then raise SelectIdConflictsWithForAll (#1 (ListPair.unzip gselect),
|
#1 (ListPair.unzip forall))
|
#1 (ListPair.unzip forall))
|
else let
|
else let
|
val (trans, fall)=ListPair.unzip (map
|
val (trans, fall)=ListPair.unzip (map
|
(makeTrans cinv_fall
|
(makeTrans cinv_fall
|
(actselect, forall, gselect, partition, action))
|
(actselect, forall, gselect, partition, action))
|
dnf)
|
dnf)
|
(* NB: forall and gselect are switched! (after having ensured
|
(* NB: forall and gselect are switched! (after having ensured
|
* names are disjoint, and `non-conflicting') *)
|
* names are disjoint, and `non-conflicting') *)
|
|
|
val _ = Util.debugVeryDetailed (fn()=>
|
val _ = Util.debugVeryDetailed (fn()=>
|
"* CETrans.negate after (&& with invariant):\n"
|
"* CETrans.negate after (&& with invariant):\n"
|
::map toString trans)
|
::map toString trans)
|
|
|
val splitFAlls=pairwiseIntersect (fall, emptyset)
|
val splitFAlls=pairwiseIntersect (fall, emptyset)
|
in
|
in
|
if AtomSet.isEmpty splitFAlls then trans
|
if AtomSet.isEmpty splitFAlls then trans
|
else (Util.warn ["forall bindings ",
|
else (Util.warn ["forall bindings ",
|
ListFormat.fmt {init="(", sep=", ", final=")",
|
ListFormat.fmt {init="(", sep=", ", final=")",
|
fmt=Atom.toString}
|
fmt=Atom.toString}
|
(AtomSet.listItems splitFAlls),
|
(AtomSet.listItems splitFAlls),
|
" are shared across disjuncts: possible split zones"];
|
" are shared across disjuncts: possible split zones"];
|
(* TODO: increase the accuracy of this detection
|
(* TODO: increase the accuracy of this detection
|
* and implement the construction from
|
* and implement the construction from
|
* thesis chapter to handle them. *)
|
* thesis chapter to handle them. *)
|
[CETrans {actselect=actselect,
|
[CETrans {actselect=actselect,
|
gselect=forall,
|
gselect=forall,
|
forall=gselect @ cinv_fall,
|
forall=gselect @ cinv_fall,
|
partition=partition,
|
partition=partition,
|
guard=e,
|
guard=e,
|
action=action,
|
action=action,
|
names=names ++ addNameTypes cinv_fall}])
|
names=names ++ addNameTypes cinv_fall}])
|
(* An improvement would be to split where possible,
|
(* An improvement would be to split where possible,
|
i.e. partition on shared foralls, transitive on overlap. *)
|
i.e. partition on shared foralls, transitive on overlap. *)
|
end
|
end
|
end
|
end
|
end (* local *)
|
end (* local *)
|
|
|
local (*{{{1*)
|
local (*{{{1*)
|
fun equateActions ([], [], e) = e
|
fun equateActions ([], [], e) = e
|
| equateActions (AT.FreeExprSub e1::ss1, AT.FreeExprSub e2::ss2, e) =
|
| equateActions (AT.FreeExprSub e1::ss1, AT.FreeExprSub e2::ss2, e) =
|
if E.equal (e1, e2)
|
if E.equal (e1, e2)
|
then equateActions (ss1, ss2, e)
|
then equateActions (ss1, ss2, e)
|
else let
|
else let
|
val eq = E.RelExpr {left=e1, rel=E.EqOp, right=e2}
|
val eq = E.RelExpr {left=e1, rel=E.EqOp, right=e2}
|
val e' = if E.equal (e, E.trueExpr) then eq
|
val e' = if E.equal (e, E.trueExpr) then eq
|
else E.BinBoolExpr {left=e, bop=E.AndOp, right=eq}
|
else E.BinBoolExpr {left=e, bop=E.AndOp, right=eq}
|
in equateActions (ss1, ss2, e') end
|
in equateActions (ss1, ss2, e') end
|
|
|
| equateActions ((AT.SelectSub _)::ss1, (AT.SelectSub _)::ss2, e) =
|
| equateActions ((AT.SelectSub _)::ss1, (AT.SelectSub _)::ss2, e) =
|
equateActions (ss1, ss2, e)
|
equateActions (ss1, ss2, e)
|
|
|
| equateActions _ = raise Fail "equateActions: assumptions not met"
|
| equateActions _ = raise Fail "equateActions: assumptions not met"
|
|
|
fun distinguishActions (ss1, ss2, e) = let
|
fun distinguishActions (ss1, ss2, e) = let
|
val ne = E.negate (equateActions (ss1, ss2, E.trueExpr))
|
val ne = E.negate (equateActions (ss1, ss2, E.trueExpr))
|
in
|
in
|
if E.equal (e, E.trueExpr) then ne
|
if E.equal (e, E.trueExpr) then ne
|
else E.BinBoolExpr {left=e, bop=E.AndOp, right=ne}
|
else E.BinBoolExpr {left=e, bop=E.AndOp, right=ne}
|
end
|
end
|
|
|
fun equateClass (x::xs, e) = let
|
fun equateClass (x::xs, e) = let
|
fun equate (x', e) = equateActions (x, x', e)
|
fun equate (x', e) = equateActions (x, x', e)
|
in foldl equate e xs end
|
in foldl equate e xs end
|
|
|
(* Form an expression that equates all members of the same class.
|
(* Form an expression that equates all members of the same class.
|
e.g. given: [ [ [e1, e2], [f1, f2], [g1, g2] ],
|
e.g. given: [ [ [e1, e2], [f1, f2], [g1, g2] ],
|
[ [h1, h2], [i1, i2] ] ]
|
[ [h1, h2], [i1, i2] ] ]
|
|
|
returns: (e1 == f1) && (e2 == f2)
|
returns: (e1 == f1) && (e2 == f2)
|
&& (e1 == g1) && (e2 == g2)
|
&& (e1 == g1) && (e2 == g2)
|
&& (h1 == i1) && (h2 == i2) *)
|
&& (h1 == i1) && (h2 == i2) *)
|
val equateClasses = foldl equateClass E.trueExpr
|
val equateClasses = foldl equateClass E.trueExpr
|
|
|
(* Form an expression that distinguish classes across a partition,
|
(* Form an expression that distinguish classes across a partition,
|
e.g. given: [ [ [e1, e2], [f1, f2], [g1, g2] ],
|
e.g. given: [ [ [e1, e2], [f1, f2], [g1, g2] ],
|
[ [h1, h2], [i1, i2] ]
|
[ [h1, h2], [i1, i2] ]
|
[ [j1, j2], [k1, k2] ] ]
|
[ [j1, j2], [k1, k2] ] ]
|
|
|
returns: e && !((e1 == h1) && (e2 == h2))
|
returns: e && !((e1 == h1) && (e2 == h2))
|
&& !((e1 == j1) && (e2 == j2))
|
&& !((e1 == j1) && (e2 == j2))
|
&& !((h1 == j1) && (h2 == j2)) *)
|
&& !((h1 == j1) && (h2 == j2)) *)
|
fun distinguishClasses ([c], e) = e
|
fun distinguishClasses ([c], e) = e
|
| distinguishClasses ((cRep::_)::cs, e) = let
|
| distinguishClasses ((cRep::_)::cs, e) = let
|
fun distinguish (oRep::_, e) = distinguishActions (cRep, oRep, e)
|
fun distinguish (oRep::_, e) = distinguishActions (cRep, oRep, e)
|
in
|
in
|
distinguishClasses (cs, foldl distinguish e cs)
|
distinguishClasses (cs, foldl distinguish e cs)
|
end
|
end
|
|
|
(* Given a partition of action subscripts, form an expression that
|
(* Given a partition of action subscripts, form an expression that
|
distinguishes the partition from others. *)
|
distinguishes the partition from others. *)
|
fun formPartitionExpr part = distinguishClasses (part, equateClasses part)
|
fun formPartitionExpr part = distinguishClasses (part, equateClasses part)
|
|
|
fun projActions partition = let
|
fun projActions partition = let
|
fun projAction (CETrans {action, ...}) = action
|
fun projAction (CETrans {action, ...}) = action
|
in map (fn class=> map projAction class) partition end
|
in map (fn class=> map projAction class) partition end
|
|
|
fun markPartition (CETrans {actselect, gselect, forall, partition,
|
fun markPartition (CETrans {actselect, gselect, forall, partition,
|
guard, action, names}, partexpr) =
|
guard, action, names}, partexpr) =
|
CETrans {actselect=actselect, gselect=gselect, forall=forall,
|
CETrans {actselect=actselect, gselect=gselect, forall=forall,
|
partition=partexpr, guard=guard, action=action, names=names}
|
partition=partexpr, guard=guard, action=action, names=names}
|
|
|
fun renameConflicts ren args = let
|
fun renameConflicts ren args = let
|
(* args: names_to_check * [] * expr_to_rename_in * conflict_set * usednames *)
|
(* args: names_to_check * [] * expr_to_rename_in * conflict_set * usednames *)
|
fun doit ([], done, g, conflicts, used) = (rev done, g, used)
|
fun doit ([], done, g, conflicts, used) = (rev done, g, used)
|
| doit ((s as (n, ty))::ss, done, g, conflicts, used) =
|
| doit ((s as (n, ty))::ss, done, g, conflicts, used) =
|
if n <- conflicts
|
if n <- conflicts
|
then let val n' = getNewName (n, used)
|
then let val n' = getNewName (n, used)
|
val g' = ren ({old=n, new=n'}, g)
|
val g' = ren ({old=n, new=n'}, g)
|
in
|
in
|
doit (ss, (n', ty)::done, g', conflicts, used <+ n')
|
doit (ss, (n', ty)::done, g', conflicts, used <+ n')
|
end
|
end
|
else doit (ss, s::done, g, conflicts, used)
|
else doit (ss, s::done, g, conflicts, used)
|
in doit args end
|
in doit args end
|
|
|
fun mergeTrans partexpr
|
fun mergeTrans partexpr
|
(CETrans {actselect=asel1, gselect=gsel1, forall=fa1,
|
(CETrans {actselect=asel1, gselect=gsel1, forall=fa1,
|
partition=p1, guard=g1, action=act1, names=n1},
|
partition=p1, guard=g1, action=act1, names=n1},
|
CETrans {actselect=asel2, gselect=gsel2, forall=fa2,
|
CETrans {actselect=asel2, gselect=gsel2, forall=fa2,
|
partition=p2, guard=g2, action=act2, names=n2}) =
|
partition=p2, guard=g2, action=act2, names=n2}) =
|
let
|
let
|
val asel1names = addNameTypes asel1
|
val asel1names = addNameTypes asel1
|
val clash = asel1names ++ addNameTypes gsel1 ++ addNameTypes fa1
|
val clash = asel1names ++ addNameTypes gsel1 ++ addNameTypes fa1
|
val (gsel2', g2', names') = renameConflicts ClkE.rename
|
val (gsel2', g2', names') = renameConflicts ClkE.rename
|
(gsel2, [], g2, clash, n1++n2)
|
(gsel2, [], g2, clash, n1++n2)
|
val (fa2', g2', names') = renameConflicts ClkE.rename
|
val (fa2', g2', names') = renameConflicts ClkE.rename
|
(fa2, [], g2', clash, names')
|
(fa2, [], g2', clash, names')
|
in
|
in
|
CETrans {actselect=asel1
|
CETrans {actselect=asel1
|
@ List.filter (fn (n,_)=> not (n<- asel1names)) asel2,
|
@ List.filter (fn (n,_)=> not (n<- asel1names)) asel2,
|
(* probably unnecessary after ATrans.ensureConsistency *)
|
(* probably unnecessary after ATrans.ensureConsistency *)
|
gselect=gsel1 @ gsel2',
|
gselect=gsel1 @ gsel2',
|
forall=fa1 @ fa2',
|
forall=fa1 @ fa2',
|
partition=partexpr,
|
partition=partexpr,
|
guard=ClkE.Or (g1, g2'),
|
guard=ClkE.Or (g1, g2'),
|
action=act1,
|
action=act1,
|
names=names'}
|
names=names'}
|
end
|
end
|
|
|
in (*}}}1*)
|
in (*}}}1*)
|
(* Map each class in a partition to a single transition.
|
(* Map each class in a partition to a single transition.
|
All transitions are stamped with the same partition expression *)
|
All transitions are stamped with the same partition expression *)
|
fun formPartitionReps [[]] = []
|
fun formPartitionReps [[]] = []
|
| formPartitionReps trpart = let
|
| formPartitionReps trpart = let
|
val partexpr = formPartitionExpr (projActions trpart)
|
val partexpr = formPartitionExpr (projActions trpart)
|
val mergeT = mergeTrans partexpr
|
val mergeT = mergeTrans partexpr
|
fun mergeClass (c::cs) = foldl mergeT (markPartition (c, partexpr)) cs
|
fun mergeClass (c::cs) = foldl mergeT (markPartition (c, partexpr)) cs
|
in map mergeClass trpart end
|
in map mergeClass trpart end
|
end (* local *)
|
end (* local *)
|
|
|
end
|
end
|
end
|
end
|
|
|
|
|