source: to-imperative/trunk/compiler/rfp_as2as.rf @ 1706

Last change on this file since 1706 was 1706, checked in by orlov, 16 years ago
  • Property svn:eol-style set to native
  • Property svn:keywords set to Author Date Id Revision
File size: 58.3 KB
Line 
1// $Source$
2// $Revision: 1706 $
3// $Date: 2005-02-02 12:12:33 +0000 (Wed, 02 Feb 2005) $
4
5$use "rfpc";
6$use "rfp_compile";
7$use "rfp_format";
8$use "rfp_helper";
9$use "rfp_vars";
10
11$use Arithm Class List StdIO Table;
12
13// transform only e.targets and leave all the rest as it is
14$func Transform (e.targets) e.Items = e.Items;
15
16// transform { A; } : Pe into { A; } :: aux, aux : Pe
17$func Unstick-Blocks e.Sentence = e.Sentence (e.Fe);
18
19$func Generate-In-Vars (e.in) e.branch = (e.in) e.branch;
20
21// rename variables local for the {}-blocks
22//$func Rename-Vars s.num (e.upper-vars) (e.res-vars) e.Snt = e.new-Snt;
23$func Rename-Vars e = e;
24
25// is variable with e.QualifiedName in the e.vars list?
26//$func? Old-Var? e.vars (s t (e.QualifiedName)) = ;
27$func? Old-Var? e = e;
28
29//$func Rename s.num (s.tag t.p (e.QualifiedName)) =
30//                      (s.tag t.p ("ren" e.QualifiedName s.num));
31$func Rename e = e;
32
33// build substitution for all occurrences of each e.var in e.Snt
34$func Build-Subst (e.vars) (e.substs) e.Snt = (e.patterns) (e.replacements);
35
36// build substitution for all occurrences of variable with the name t.n in e.Snt
37$func Var-Subst t.n t.s e.Snt = (e.patterns) (e.replacements);
38
39
40RFP-As2As-Transform e.Items =
41  { <Lookup &RFP-Options ITEMS>;; } :: e.targets,
42  <Transform (e.targets) e.Items>;
43
44Transform (e.targets) e.Items, {
45  e.Items : t.item e.rest, {
46    {
47      e.targets : v =
48        e.targets : e t.name e,
49        t.item : (t t t t.name e);;
50    },
51      t.item : (s.link s.tag t.pragma t.name (e.in) (e.out) (BRANCH t.p e.branch)) =
52      <Unstick-Blocks e.branch> :: e.branch t,
53      {
54        <Format-Exp e.in> : e.in =
55          <Generate-In-Vars (e.in) e.branch>;
56        (e.in) e.branch;
57      } :: (e.in) e.branch,
58      <Rename-Vars 0 (<Vars e.in>) () e.branch> :: e.branch,
59      (s.link s.tag t.pragma t.name (e.in) (e.out) (BRANCH t.p e.branch));
60    t.item;
61  } :: t.item =
62    t.item <Transform (e.targets) e.rest>;;
63};
64
65/*
66 * Next function gets use of the following proposition:
67 *  one can add (RESULT) term to the end of any sentence that isn't end in
68 *  (RESULT e.anything) and it won't change the result of program execution.
69 * No, no, the proposition is WRONG!!! Such doings change the semantics of "=".
70 *
71 * The function returns the sentence with all { A; } : Pe constructions
72 * turned into { A; } :: aux, aux : Pe ones and format of the last Re of
73 * the sentence.
74 */
75Unstick-Blocks e.Sentence, e.Sentence : eL e.Snt, e.Snt : \{
76  (s.block t.Pragma e.branches) eR, s.block : \{ BLOCK; BLOCK?; } =
77    e.branches () () $iter {
78      e.branches : (BRANCH t.p e.branch) e.rest,
79        <Unstick-Blocks e.branch> :: e.new-branch (e.Fe),
80        { e.Fe : FAIL; (e.Fe); } :: e.Fe,
81        e.rest (e.br (BRANCH t.p e.new-branch)) (e.Fes e.Fe);
82    } :: e.branches (e.br) (e.Fes),
83    e.branches : /*empty*/ =
84    {
85      eR : \{
86        (BLOCK  t (BRANCH t (LEFT e) e) e) e;
87        (BLOCK  t (BRANCH t (RIGHT e) e) e) e;
88        (BLOCK? t (BRANCH t (LEFT e) e) e) e;
89        (BLOCK? t (BRANCH t (RIGHT e) e) e) e;
90        (LEFT e) e;
91        (RIGHT e) e;
92      } =
93        <Gener-Var-Indices 1 (<MSG e.Fes>) "aux" "block"> :: e.aux s,
94        eL (s.block t.Pragma e.br) (FORMAT e.aux)
95        (RESULT e.aux) <Unstick-Blocks eR>;
96      eR : /*empty*/ =
97        eL (s.block t.Pragma e.br) (<MSG e.Fes>);
98      eL (s.block t.Pragma e.br) <Unstick-Blocks eR>;
99    };
100  (RESULT t.Pragma e.Re) =
101    eL (RESULT t.Pragma e.Re) (<Format-Exp e.Re>);
102  (ITER (BRANCH t.p1 e.body) t.IterVars (BRANCH t.p2 e.condition)) =
103    <Unstick-Blocks e.body> :: e.body t,
104    <Unstick-Blocks e.condition> :: e.condition (e.Format),
105    eL (ITER (BRANCH t.p1 e.body) t.IterVars (BRANCH t.p2 e.condition)) (e.Format);
106  (TRY (BRANCH t.p1 e.TrySnt) e.NOFAIL t.CatchBlock) =
107    <Unstick-Blocks e.TrySnt> :: e.TrySnt t.Try-Fe,
108    <Unstick-Blocks t.CatchBlock> :: e.CatchBlock t.Catch-Fe,
109    eL (TRY (BRANCH t.p1 e.TrySnt) e.NOFAIL e.CatchBlock) (<MSG t.Try-Fe t.Catch-Fe>);
110  (FAIL e) = e.Sentence (FAIL);
111  (ERROR t.Pragma) eR =
112    <Unstick-Blocks eR> :: eR t,
113    eL (ERROR t.Pragma) eR (FAIL);
114};
115
116/*
117 * Generate variable names for input function parameters. Change e.Sentence so
118 * that it doesn't begin with pattern.
119 */
120Generate-In-Vars (e.in) e.Sentence, {
121  /*
122   * If input PAlt of a function is a sentence (not a block), format of
123   * input pattern coincides t.InputFormat, and all variables in input
124   * pattern have different indexes then we can drop the pattern and define
125   * function as
126   *    func (Fname (pattern_vars) (res_..., res_..., ...))
127   * where pattern_vars means variables used in the pattern.
128   */
129  e.Sentence : \{
130    (LEFT t e.Pe) e.Snt = (e.Pe) e.Snt;
131    (RIGHT t e.Pe) e.Snt = (e.Pe) e.Snt;
132  } :: (e.Pe) e.Snt =
133    {
134      <Format-Exp e.Pe> : e.in,  // FIXME: here should be checked format equality
135        <Vars e.Pe> :: e.args,
136        # \{ e.args : e (e t1) e (e t1) e; } =
137        (e.Pe) e.Snt;
138      <Gener-Var-Indices 1 (e.in) "arg"> :: e.in-expr s =
139        (e.in-expr) (RESULT (PRAGMA) e.in-expr) e.Sentence;
140    };
141  /*
142   * Else if we have real PAlt then we can do that transformation with each
143   * branch. Input parameters for the function will be arg_1...arg_N. If
144   * first pattern in the branch satisfies the conditions then drop it out
145   * and rename variables in the branch to arg_1...arg_N instead of pattern
146   * variables.
147   */
148  e.Sentence : (s.block t.Pragma e.branches) e.Snt =
149    <Gener-Var-Indices 1 (e.in) "arg"> :: e.in-expr s,
150    <Vars e.in-expr> :: e.in-vars,
151    (/*e.br*/) e.branches $iter {
152      e.branches : (BRANCH t.p (s.dir t.pp e.Pe) e.br-snt) e.rest, {
153        <Format-Exp e.Pe> : e.in,  // FIXME: here should be checked format equality
154          <Vars e.Pe> :: e.vars,
155          # \{ e.vars : e (e t1) e (e t1) e; } =
156          <Build-Subst (e.vars) (e.in-vars) e.br-snt> :: (e.pats) (e.repls),
157          (e.br (BRANCH t.p <Subst (e.pats) (e.repls) e.br-snt>)) e.rest;
158        (e.br (BRANCH t.p (s.dir t.pp e.Pe) e.br-snt)) e.rest;
159      };
160    } :: (e.br) e.branches,
161    e.branches : /*empty*/ =
162    (e.in-expr) (s.block t.Pragma e.br) e.Snt;
163  /*
164   * Else sentence already hasn't begun with pattern, so left it as it is.
165   * It can be only if e.in and e.out are both empty.
166   */
167//!     (e.in) e.Sentence;
168} :: (e.in) e.Sentence =
169  (e.in) e.Sentence;
170
171/*
172 * Each {}-block is seen as inlined function. e.upper-vars and e.res-vars are
173 * correspondingly input and output parameters for that function. e.Snt is its
174 * body.
175 * Rename all variables local for inlined function, for those to be
176 * distinguishable from the outer world when the function is inlined in
177 * imperative language.
178 */
179Rename-Vars s.num (e.upper-vars) (e.res-vars) e.Snt =
180  (e.upper-vars) (/*e.new-Snt*/) e.Snt $iter {
181    e.Snt : t.Statement e.rest, {
182      /*
183       * If we meet a pattern then add each unknown variable from it to
184       * the list and rename local variables which intersect with out
185       * parameters of the block.
186       */
187      t.Statement : \{
188        (LEFT t e.Pe) = e.Pe;
189        (RIGHT t e.Pe) = e.Pe;
190      } :: e.Pe =
191        <Split &Old-Var? e.res-vars (<Vars e.Pe>)> :: (e.old-vars) (e.new-vars),
192        <Map &Rename s.num (e.old-vars)> :: e.renames,
193        <Build-Subst (e.old-vars) (e.renames) e.Snt> :: (e.pats) (e.repls),
194        <Subst (e.pats) (e.repls) e.Snt> : (s.tag t.p e.Pe1) e.rest-Snt,
195        (<Or (e.vars) <Vars e.Pe1>>) (e.new-Snt (s.tag t.p e.Pe1)) e.rest-Snt;
196      /*
197       * If we meet format expression then for each already used
198       * variable in it select new name by adding prefix "ren".
199       */
200      t.Statement : (FORMAT t e.He) =
201        <Split &Old-Var? e.upper-vars e.res-vars (<Vars e.He>)>
202          :: (e.old-vars) (e.new-vars),
203        <Map &Rename s.num (e.old-vars)> :: e.renames,
204        <Build-Subst (e.old-vars) (e.renames) e.Snt> :: (e.pats) (e.repls),
205        <Subst (e.pats) (e.repls) e.Snt> : (FORMAT t.p e.He1) e.rest-Snt,
206        (<Or (e.vars) <Vars e.He1>>) (e.new-Snt (FORMAT t.p e.He1)) e.rest-Snt;
207      /*
208       * We shouldn't rename variable if its duplicate is appeared on
209       * a parallel branch of the block. So process all branches
210       * iteratively with the same list of variables (known before
211       * block).
212       */
213      t.Statement : (s.block t.Pragma e.branches), s.block : \{ BLOCK; BLOCK?; } =
214        /*
215         * As well as after-block patterns, formats should be scaned
216         * for res-vars.  See samples/Syntax/block1.rf for example.
217         */
218        e.rest : {
219          (LEFT t e.Pe) e = <Vars e.Pe>;
220          (RIGHT t e.Pe) e = <Vars e.Pe>;
221          (FORMAT t e.He) e = <Vars e.He>;
222          /*empty*/ = e.res-vars;
223          e = /*empty*/;
224        } :: e.bl-res-vars,
225        /*
226         * Left as res-vars only variables which were unknown before
227         * block. Those are local if meet in pattern and need
228         * renaming.
229         */
230        (/*e.brv*/) e.bl-res-vars $iter {
231          e.bl-res-vars : e1 (e t.name) e2, e.vars : e (e t.name) e =
232            (e.brv e1) e2;
233          (e.brv e.bl-res-vars);
234        } :: (e.brv) e.bl-res-vars,
235        e.bl-res-vars : /*empty*/ =
236        <Map &Rename-Vars <"+" s.num 1> (e.vars) (e.brv) (e.branches)>
237          :: e.branches,
238        (e.vars) (e.new-Snt (s.block t.Pragma e.branches)) e.rest;
239      t.Statement : (BRANCH t.Pragma e.Sentence) =
240        () (e.new-Snt (BRANCH t.Pragma
241            <Rename-Vars s.num (e.vars) (e.res-vars) e.Sentence>));
242      t.Statement : (ITER t.IterBody t.IterVars t.IterCondition) =
243        <Rename-Vars
244          s.num (e.upper-vars) (e.res-vars) t.IterVars t.IterBody
245        > : t t.NewBody,
246        <Rename-Vars
247          s.num (e.upper-vars) (e.res-vars) t.IterVars t.IterCondition
248        > :: e.IterCondition,
249        () (e.new-Snt (ITER t.NewBody e.IterCondition));
250      t.Statement : (TRY t.TryBranch e.NOFAIL t.Catch) =
251        <Rename-Vars s.num (e.upper-vars) (e.res-vars) t.TryBranch> :: e.TryBranch,
252        <Rename-Vars s.num (e.upper-vars) (e.res-vars) t.Catch> :: e.Catch,
253        () (e.new-Snt (TRY e.TryBranch e.NOFAIL e.Catch));
254      /*
255       * Else proceed with the rest.
256       */
257      (e.vars) (e.new-Snt t.Statement) e.rest;
258    };
259  } :: (e.vars) (e.new-Snt) e.Snt,
260  e.Snt : /*empty*/ =
261  e.new-Snt;
262
263Old-Var? e.vars (s.tag t (e.QualifiedName)) = e.vars : e (s.tag t (e.QualifiedName)) e;
264
265Rename s.num (s.tag t.p (e.QualifiedName)) =
266  (s.tag t.p (e.QualifiedName "_" s.num));
267
268/*
269 * Build substitution for all occurrences of each e.var in e.Snt.
270 */
271Build-Subst {
272  ((s t t.name) e.vars) ((s t t.s) e.substs) e.Snt =
273    <Var-Subst t.name t.s e.Snt> :: (e.var-pats) (e.var-repls),
274    <Build-Subst (e.vars) (e.substs) e.Snt> :: (e.pats) (e.repls),
275    (e.var-pats e.pats) (e.var-repls e.repls);
276  () () e = () ();
277};
278
279/*
280 * Build substitution for all occurrences of variable with the name t.n in e.Snt.
281 */
282Var-Subst t.n t.s e.Snt, {
283  e.Snt : t.Statement e.rest, {
284    t.Statement : \{
285      (SVAR t.p t.name) = SVAR t.p t.name;
286      (TVAR t.p t.name) = TVAR t.p t.name;
287      (VVAR t.p t.name) = VVAR t.p t.name;
288      (EVAR t.p t.name) = EVAR t.p t.name;
289    } :: s.tag t.p t.name,
290      {
291        t.name : t.n = ((s.tag t.p t.name)) (((s.tag t.p t.s)));
292        () ();
293      };
294    t.Statement : (expr) = <Var-Subst t.n t.s expr>;
295    () ();
296  } :: (e.st-pats) (e.st-repls),
297    <Var-Subst t.n t.s e.rest> :: (e.pats) (e.repls),
298    (e.st-pats e.pats) (e.st-repls e.repls);
299  () ();
300};
301
302
303/////////////////////////// Varibles Using Analysis /////////////////////////
304//
305//$func Post-Comp (e.used-vars) e.comp-func = (e.used-vars) e.result-func;
306//
307//Post-Comp (e.used-vars) e.comp-func, e.comp-func : {
308//  /*
309//   * As well as "Used" shouldn't be "Declare" statements added?
310//   */
311//  e.something (Used e.vars) =
312//    <Post-Comp (<Or (e.used-vars) e.vars>) e.something>;
313//  e.something (If-used (e.vars) e.statements), {
314//    <Split &Elem? e.vars (e.used-vars)> : (v.true-used) (e.yet-not-used) =
315//      <Post-Comp (v.true-used) e.statements> :: (e.expr-vars) e.expr,
316//      <Post-Comp (<Or (e.yet-not-used) e.expr-vars>) e.something> e.expr;
317//    <Post-Comp (e.used-vars) e.something>;
318//  };
319//  e.something (e.expr) =
320//    <Post-Comp (e.used-vars) e.expr> :: (e.expr-vars) e.expr,
321//    <Post-Comp (e.expr-vars) e.something> (e.expr);
322//  e.something s.symbol =
323//    <Post-Comp (e.used-vars) e.something> s.symbol;
324//  /*empty*/ = (e.used-vars);
325//};
326
327
328/////////////////////////// Static Clash Analysis ///////////////////////////
329//
330//$func? Split-Clashes (e.clashes) e.Snt =
331//  (e.greater) (e.less) (e.hards) (e.clashes) e.Snt;
332//
333//$func? Improve-Clash (e.Re) (s.dir e.Pe) (e1) (e2) e.Snt = e.clashes (e.Snt);
334//
335//$func? Self-Occur (e.Re) e.Pe = e;
336//
337//$func Cyclic e.expr = e.cyclic-vars;
338//
339//$func Hard e.expr = e.hard-part;
340//
341//$func Exchange (e.var-holder) (e.new-expr) e.clashes (e.Snt) =
342//  e.clashes (e.Snt);
343//
344//$func Exchange-Exp (e.change) (e1) (e2) e.Snt = (e1) (e2) e.Snt;
345//
346//$func Minimize (e.expr) (e.clashes) e.Snt = (e.clashes) (e.less) e.Snt;
347//
348//$func? Intersect s.k (e.l) s.m (e.n) = s.x (e.y);
349//
350//$func Min-Length e.expr = s.min-length;
351//
352//$func Max-Length e.expr = e.max-length;
353//
354//$func? Add-Less-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt =
355//  (e.clashes1) (e.clashes2) e.Snt;
356//
357//$func? Add-Greater-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt =
358//  (e.clashes1) (e.clashes2) e.Snt;
359//
360//$func Get-Min e.vars = s.min;
361//
362//$func Get-Max e.vars = e.max;
363//
364//$func Mults e.vars = e.mults;
365//
366//$func Mark-Unw-Hard (e.vars) e.clashes = e.clashes;
367//
368//$func Ceil s1 s2 = s;
369//
370//$func? Match-Exp (e.Re) e.Pe = s.left s.right;
371//
372//$func? Match e.clash = ;
373//
374//$func? Match-Term t.Rt t.Pt e.clashes = e.clashes;
375//
376//$func? Match-Cyclic (e.Re) (e.Pe) e.clashes = e.clashes;
377//
378//$func Granulate e.expr = e.expr;
379//
380//$func? Left-Exp s.left s.len e.expr = (e.expr) e.change;
381//
382//$func? Right-Exp s.right s.len e.expr = (e.expr) e.change;
383//
384//$func? Middle-Exp s.left s.right e.expr = (e.expr) e.change;
385//
386*$func Comp-Pattern t.Pattern e.Snt = e.asail-Snt;
387*
388*Comp-Pattern (s.dir e.PatternExp) e.Sentence =
389*       <Norm-Vars (<Vars e.PatternExp>) (s.dir e.PatternExp) e.Sentence>
390*               : t t.Pattern e.Snt,
391*//     (Unwatched (<? &Last-Re>) t.Pattern) e.Snt $iter {
392*       /*
393*        * Uncomment previous line and delete next one to activate Split-Clashes
394*        * function
395*        */
396*       ((<? &Last-Re>) t.Pattern) e.Snt $iter {
397*               e.Snt : (RESULT e.Re) (s.d e.Pe) e =
398*//                     <WriteLN Matching (RESULT e.Re) (s.d e.Pe)>,
399*                       <Norm-Vars (<Vars e.Pe>) e.Snt> : t t.R t.P e.rest,
400*//                     (e.clashes Unwatched (e.Re) t.P) e.rest;
401*                       /*
402*                        * Uncomment previous line and delete next one to activate
403*                        * Split-Clashes function
404*                        */
405*                       (e.clashes (e.Re) t.P) e.rest;
406*       } :: (e.clashes) e.Snt,
407*       # \{
408*               e.Snt : \{
409*                       (RESULT e.Re) (LEFT e) e = e.Re;
410*                       (RESULT e.Re) (RIGHT e) e = e.Re;
411*               } :: e.Re,
412*                       <Without-Calls? e.Re>;
413*       } =
414*       e.Snt : e.Current-Snt (Comp Sentence) e.Other-Snts =
415*       <Comp-Sentence () e.Other-Snts> :: e.asail-Others,
416*       {
417*//             <Split-Clashes (e.clashes) e.Current-Snt>
418*//             :: (e.greater) (e.less) (e.hards) (e.clashes) e.Current-Snt =
419*//                     <WriteLN "Hards: " e.hards>,
420*//                     <WriteLN "Less: " e.less>,
421*//                     <WriteLN "Greater: " e.greater>,
422*//                     <WriteLN "Current-Snt: " e.Current-Snt>,
423*//!                    <Comp-Clashes (e.clashes)
424*//!                            (e.Current-Snt (Comp Sentence)) e.Other-Snts> :: e.asail-Clashes,
425*//                     e.asail-Clashes (e.greater) $iter {
426*//                             e.greater : (e.vars s.num) e.rest,
427*//                                     <Old-Vars e.vars> :: e.vars,  // temporary step
428*//                                     (IF ((INFIX ">=" ((LENGTH e.vars)) (s.num)))
429*//                                             e.asail-Clashes
430*//                                     ) (e.rest);
431*//                     } :: e.asail-Clashes (e.greater),
432*//                     e.greater : /*empty*/ =
433*//                     e.asail-Clashes (e.less) $iter {
434*//                             e.less : (e.vars s.num) e.rest,
435*//                                     <Old-Vars e.vars> :: e.vars,  // temporary step
436*//                                     (IF ((INFIX "<=" ((LENGTH e.vars)) (s.num)))
437*//                                             e.asail-Clashes
438*//                                     ) (e.rest);
439*//                     } :: e.asail-Clashes (e.less),
440*//                     e.less : /*empty*/ =
441*//                     e.asail-Clashes (e.hards) $iter {
442*//                             e.hards : (e.Re) (e.Pe) e.rest,
443*//                                     <Old-Vars e.Re> :: e.Re,    // temporary step
444*//                                     <Old-Vars e.Pe> :: e.Pe,    // temporary step
445*//                                     (IF ((INFIX "==" (e.Re) (e.Pe))) e.asail-Clashes) (e.rest);
446*//                     } :: e.asail-Clashes (e.hards),
447*//                     e.hards : /*empty*/ =
448*//!                    e.asail-Clashes e.asail-Others;
449*               e.asail-Others;
450*//             <Comp-Sentence () e.Other-Snts>;
451*       };
452//
453//Split-Clashes (e.clashes) e.Snt =
454//  e.clashes (e.Snt) () () () $iter e.clashes : {
455//    e1 Unwatched (e.Re) (s.dir e.Pe) e2, { \?
456//      \{
457//        \{
458//          <Self-Occur (e.Re) e.Pe> : {
459//            Occur e.vars =
460//              <Minimize (e.vars) (e1 e2) e.Snt>
461//                :: (e.clashes) (e.new-less) e.Snt,
462//              e.clashes (e.Snt)
463//              (e.greater) (e.less e.new-less) (e.hards);
464//            /*empty*/ \! $fail;
465//          };
466//          <Self-Occur (e.Pe) e.Re> : {
467//            Occur e.vars =
468//              <Minimize (e.vars) (e1 e2) e.Snt>
469//                :: (e.clashes) (e.new-less) e.Snt,
470//              e.clashes (e.Snt)
471//              (e.greater) (e.less e.new-less) (e.hards);
472//            /*empty*/ \! $fail;
473//          };
474//        };
475//        <Vars e.Re> : /*empty*/, \{ // e.Re is ground expression
476//          <Vars e.Pe> : /*empty*/ \! // e.Pe is ground expression
477//            $fail;
478//          e.Pe : \{
479//            /*
480//             * If e.Pe is symbol then e.Re should be a symbol and if
481//             * e.Pe is "old" variable then we should remember clash
482//             * "e.Re : e.Pe" as hard.
483//             */
484//            (SVAR 1 (1) e.name) \!
485//              e.Re : s,
486//              {
487//                <Known-Vars? (SVAR e.name)> = (e.Re) (e.Pe);
488//                /*empty*/;
489//              } :: e.new-hard,
490//              <Exchange (e.Pe) (e.Re) e1 e2 (e.Snt)>
491//                (e.greater) (e.less) (e.hards e.new-hard);
492//            /*
493//             * If e.Pe is parenthesized expression then e.Re should be
494//             * parenthesized expression too and we can take parentheses
495//             * off.
496//             */
497//            (PAREN e.pat-expr) \!
498//              e.Re : (PAREN e.re-expr),
499//              e1 Unwatched (e.re-expr) (s.dir e.pat-expr) e2
500//              (e.Snt) (e.greater) (e.less) (e.hards);
501//            /*
502//             * If e.Pe is any other variable then length of e.Re (which
503//             * can be zero) should belong to its range. If e.Pe is
504//             * "old" variable and e.Re is empty expression then we
505//             * should remember that length of e.Pe is less or equal to
506//             * 0 and if e.Re isn't empty then we should remember clash
507//             * "e.Re : e.Pe" as hard.
508//             */
509//            (s.var-tag s.m (e.n) e.name) \!
510//              <Intersect s.m (e.n) <Length e.Re> (<Length e.Re>)> : e,
511//              {
512//                <Known-Vars? (s.var-tag e.name)>,
513//                  {
514//                    e.Re : /*empty*/ = (e.Pe 0) ();
515//                    /*empty*/ ((e.Re) (e.Pe));
516//                  };
517//                /*empty*/ ();
518//              } :: e.new-less (e.new-hard),
519//              <Exchange (e.Pe) (e.Re) e1 e2 (e.Snt)>
520//              (e.greater) (e.less e.new-less) (e.hards e.new-hard);
521//          };
522//        };
523//        <Vars e.Pe> : /*empty*/, e.Re : \{
524//          (SVAR 1 (1) e.name) \!
525//            e.Pe : s,
526//            {
527//              <Known-Vars? (SVAR e.name)> = (e.Re) (e.Pe);
528//              /*empty*/;
529//            } :: e.new-hard,
530//            <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
531//              (e.greater) (e.less) (e.hards e.new-hard);
532//          (PAREN e.re-expr) \!
533//            e.Pe : (PAREN e.pe-expr),
534//            e1 Unwatched (e.re-expr) (s.dir e.pe-expr) e2
535//            (e.Snt) (e.greater) (e.less) (e.hards);
536//          (s.var-tag s.m (e.n) e.name) \!
537//            <Intersect s.m (e.n) <Length e.Pe> (<Length e.Pe>)> : e,
538//            {
539//              <Known-Vars? (s.var-tag e.name)>,
540//                {
541//                  e.Pe : /*empty*/ = (e.Re 0) ();
542//                  /*empty*/ ((e.Re) (e.Pe));
543//                };
544//              /*empty*/ ();
545//            } :: e.new-less (e.new-hard),
546//            <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
547//            (e.greater) (e.less e.new-less) (e.hards e.new-hard);
548//        };
549//        e.Re : \{
550//          (PAREN e.re-expr), e.Pe : \{
551//            (PAREN e.pe-expr) =
552//              e1 Unwatched (e.re-expr) (s.dir e.pe-expr) e2
553//              (e.Snt) (e.greater) (e.less) (e.hards);
554//            (SVAR e) \!
555//              $fail;
556//            (s.tag s.m (e.n) e.var-id) \!
557//              e.var-id : e.NEW (e.QualifiedName),
558//              <Intersect 1 (1) s.m (e.n)> :: e,
559//              (s.tag 0 () NEW ("paren" e.QualifiedName)) :: t.new-var,
560//              {
561//                <Known-Vars? (s.tag e.var-id)> =
562//                  Watched (e.Pe) (s.dir (PAREN t.new-var));
563//                /*empty*/;
564//              } :: e.new-clash,
565//              <Exchange (e.Pe) ((PAREN t.new-var)) e1 ()> :: e1 t,
566//              e.new-clash e1 Unwatched (e.re-expr) (s.dir t.new-var)
567//              <Exchange (e.Pe) ((PAREN t.new-var)) e2 (e.Snt)>
568//              (e.greater) (e.less) (e.hards);
569//          };
570//          (SVAR 1 (1) e.name), e.Pe : \{
571//            s.ObjectSymbol =
572//              {
573//                <Known-Vars? (SVAR e.name)> = (e.Re) (e.Pe);
574//                /*empty*/;
575//              } :: e.new-hard,
576//              <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
577//              (e.greater) (e.less) (e.hards e.new-hard);
578//            (PAREN e) \!
579//              $fail;
580//            (s.tag s.m (e.n) e.var-id) \!
581//              <Intersect 1 (1) s.m (e.n)> :: e,
582//              {
583//                <Known-Vars? (s.tag e.var-id)>, {
584//                  <Known-Vars? (SVAR e.name)> =
585//                    ((e.Re) (e.Pe)) ();
586//                  () (Watched (e.Pe) (s.dir e.Re));
587//                };
588//                () ();
589//              } :: (e.new-hard) (e.new-clash),
590//              e.new-clash <Exchange (e.Pe) (e.Re) e1 e2 (e.Snt)>
591//              (e.greater) (e.less) (e.hards e.new-hard);
592//          };
593//          (s.tag s.m (e.n) e.var-id), TVAR VVAR EVAR : e s.tag e, \{
594//            e.Pe : (s.tag1 s.k (e.l) e.var-id1),
595//              TVAR VVAR EVAR : e s.tag1 e \!
596//              <Intersect s.m (e.n) s.k (e.l)> :: s.x (e.y),
597//              {
598//                <Known-Vars? (s.tag e.var-id)>, {
599//                  <Known-Vars? (s.tag1 e.var-id1)> =
600//                    (s.tag s.x (e.y) e.var-id) (e.Re) (e.Pe);
601//                  (s.tag s.x (e.y) e.var-id) /*empty*/;
602//                };
603//                (s.tag1 s.x (e.y) e.var-id1) /*empty*/;
604//              } :: t.new-var e.new-hards,
605//              <Exchange (e.Re) (t.new-var) e1 e2 (e.Snt)>
606//                :: e.clashes (e.Snt),
607//              <Exchange (e.Pe) (t.new-var) e.clashes (e.Snt)>
608//              (e.greater) (e.less) (e.hards e.new-hards);
609//          };
610//        };
611//        e.Pe : \{
612//          (PAREN e.pe-expr), e.Re : \{
613//            (s.tag s.m (e.n) e.var-id) \!
614//              e.var-id : e.NEW (e.QualifiedName),
615//              <Intersect 1 (1) s.m (e.n)> :: e,
616//              (s.tag 0 () NEW ("paren" e.QualifiedName)) :: t.new-var,
617//              {
618//                <Known-Vars? (s.tag e.var-id)> =
619//                  Watched (e.Re) (s.dir (PAREN t.new-var));
620//                /*empty*/;
621//              } :: e.new-clash,
622//              <Exchange (e.Re) ((PAREN t.new-var)) e1 ()> :: e1 t,
623//              e.new-clash e1 Unwatched (t.new-var) (s.dir e.pe-expr)
624//              <Exchange (e.Re) ((PAREN t.new-var)) e2 (e.Snt)>
625//              (e.greater) (e.less) (e.hards);
626//          };
627//          (SVAR 1 (1) e.name), e.Re : \{
628//            (s.tag s.m (e.n) e.var-id) \!
629//              <Intersect 1 (1) s.m (e.n)> :: e,
630//              {
631//                <Known-Vars? (s.tag e.var-id)>, {
632//                  <Known-Vars? (SVAR e.name)> =
633//                    ((e.Re) (e.Pe)) ();
634//                  () (Watched (e.Re) (s.dir e.Pe));
635//                };
636//                () ();
637//              } :: (e.new-hard) (e.new-clash),
638//              e.new-clash <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
639//              (e.greater) (e.less) (e.hards e.new-hard);
640//          };
641//        };
642//        e.Re : t.Rt e.Re1, e.Pe : t.Pt e.Pe1,
643//          <Min-Length t.Rt> :: s.rt-min, <Min-Length t.Pt> :: s.pt-min,
644//          # \{ s.rt-min : 0; s.pt-min : 0; } =
645//          {
646//            <Left-Exp 0 s.rt-min t.Pt> (<Left-Exp 0 s.rt-min t.Rt>);
647//            <Left-Exp 0 s.pt-min t.Rt> (<Left-Exp 0 s.pt-min t.Pt>);
648//          } :: t e.change1 (t e.change2),
649//          e1 Unwatched (e.Re) (e.Pe) :: e1,
650//          <Exchange-Exp (e.change1)
651//            <Exchange-Exp (e.change2) (e1) (e2) e.Snt>>
652//            :: (e1) (e2) e.Snt,
653//          {
654//            e.change1 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
655//              <Known-Vars? (s.tag e.var-id)> =
656//              Watched
657//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
658//            /*empty*/;
659//          } :: e.new-clash1,
660//          {
661//            e.change2 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
662//              <Known-Vars? (s.tag e.var-id)> =
663//              Watched
664//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
665//            /*empty*/;
666//          } :: e.new-clash2,
667//          e1 : e11 (t.Rt1 e.Re2) (t.Pt1 e.Pe2),
668//          e.new-clash1 e.new-clash2 e11 (t.Rt1) (s.dir t.Pt1)
669//          Unwatched (e.Re2) (s.dir e.Pe2) e2
670//          (e.Snt) (e.greater) (e.less) (e.hards);
671//        e.Re : e.Re1 t.Rt, e.Pe : e.Pe1 t.Pt,
672//          <Min-Length t.Rt> :: s.rt-min, <Min-Length t.Pt> :: s.pt-min,
673//          # \{ s.rt-min : 0; s.pt-min : 0; } =
674//          {
675//            <Right-Exp 0 s.rt-min t.Pt> (<Right-Exp 0 s.rt-min t.Rt>);
676//            <Right-Exp 0 s.pt-min t.Rt> (<Right-Exp 0 s.pt-min t.Pt>);
677//          } :: t e.change1 (t e.change2),
678//          e1 Unwatched (e.Re) (e.Pe) :: e1,
679//          <Exchange-Exp (e.change1)
680//            <Exchange-Exp (e.change2) (e1) (e2) e.Snt>>
681//            :: (e1) (e2) e.Snt,
682//          {
683//            e.change1 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
684//              <Known-Vars? (s.tag e.var-id)> =
685//              Watched
686//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
687//            /*empty*/;
688//          } :: e.new-clash1,
689//          {
690//            e.change2 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
691//              <Known-Vars? (s.tag e.var-id)> =
692//              Watched
693//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
694//            /*empty*/;
695//          } :: e.new-clash2,
696//          e1 : e11 (e.Re2 t.Rt1) (e.Pe2 t.Pt1),
697//          e.new-clash1 e.new-clash2 e11 (e.Re2) (s.dir e.Pe2)
698//          Unwatched (t.Rt1) (s.dir t.Pt1) e2
699//          (e.Snt) (e.greater) (e.less) (e.hards);
700//        <Max-Length e.Re> : /*empty*/, <Max-Length e.Pe> : /*empty*/ \!
701//          <Min-Length e.Re> :: s.re-min,
702//          <Min-Length e.Pe> :: s.pe-min,
703//          e1 Unwatched Hard (e.Re) (s.dir e.Pe) :: e1,
704//          {
705//            <"<" (s.re-min) (s.pe-min)> =
706//              <Add-Greater-Ineq (<Cyclic e.Re> s.pe-min)
707//                (e1) (e2) e.Snt>;
708//            <">" (s.re-min) (s.pe-min)> =
709//              <Add-Greater-Ineq (<Cyclic e.Pe> s.re-min)
710//                (e1) (e2) e.Snt>;
711//            (e1) (e2) e.Snt;
712//          } :: (e1) (e2) e.Snt,
713//          e1 e2 (e.Snt) (e.greater) (e.less) (e.hards);
714//        {
715//          <Max-Length e.Re> : s.re-max, {
716//            <Max-Length e.Pe> : s.pe-max, {
717//              <"<" (s.re-max) (s.pe-max)> = e.Pe s.re-max;
718//              e.Re s.pe-max;
719//            };
720//            e.Pe s.re-max;
721//          };
722//          e.Re <Max-Length e.Pe>;
723//        } : e.ineq s.max \!
724//          <"-" s.max <Min-Length <Hard e.ineq>>> :: s.max,
725//          <Cyclic e.ineq> :: e.cyclic,
726//          <Add-Less-Ineq (e.cyclic s.max)
727//            (e1 Unwatched Hard (e.Re) (s.dir e.Pe)) (e2) e.Snt>
728//            :: (e1) (e2) e.Snt \?
729//          {
730//            e1 : e Unwatched Hard t t \!
731//              <Min-Length e.Re> :: s.re-min,
732//              <Min-Length e.Pe> :: s.pe-min,
733//              {
734//                <"<" (s.re-min) (s.pe-min)> = e.Re s.pe-min;
735//                e.Pe s.re-min;
736//              } :: e.ineq s.min,
737//              <"-" s.min <Min-Length <Hard e.ineq>>> :: s.min,
738//              <Cyclic e.ineq> :: e.cyclic,
739//              <Add-Greater-Ineq (e.cyclic s.min) (e1) (e2) e.Snt>
740//                :: (e1) (e2) e.Snt,
741//              e1 e2 (e.Snt) (e.greater) (e.less) (e.hards);
742//            e1 e2 (e.Snt) (e.greater) (e.less) (e.hards);
743//          };
744//      };
745//      = <Print-Error Warning! Pattern (e.Re ' : ' e.Pe)>, $fail;
746//    };
747//    e1 Unwatched Hard (e.Re) (s.dir e.Pe) e2, {
748//      <Cyclic e.Re> : /*empty*/, {  // e.Re is hard expression
749//        <Improve-Clash (e.Re) (s.dir e.Pe) (e1) (e2) e.Snt>
750//          (e.greater) (e.less) (e.hards);
751//        <Print-Error Warning! Pattern (e.Re ' : ' e.Pe)>
752//          = $fail;
753//      };
754////      <Cyclic e.Pe> : /*empty*/ = // e.Pe is hard expression
755////        <Improve-Clash (e.Pe) (e.Re) (e1) (e2) e.Snt>
756////        (e.greater) (e.less) (e.hards);
757//      e1 (e.Re) (s.dir e.Pe) e2 (e.Snt) (e.greater) (e.less) (e.hards);
758//    };
759//    e1 Watched t.Re t.Pe e2 =
760//      e1 t.Re t.Pe e2 (e.Snt) (e.greater) (e.less) (e.hards);
761//  } :: e.clashes (e.Snt) (e.greater) (e.less) (e.hards),
762////  <WriteLN Sp-Clashes e.clashes>,
763////  <WriteLN G <? &Greater-Ineqs>>,
764////  <WriteLN L <? &Less-Ineqs>>,
765//  # \{ e.clashes : e s e; } =
766//  (e.greater) (e.less) (e.hards) (e.clashes) e.Snt;
767//
768//Improve-Clash (e.Re) (s.dir e.Pe) (e1) (e2) e.Snt =
769////  <WriteLN Improve-Clash (e.Re) (s.dir e.Pe)>,
770//  /*
771//   * Find all non-empty hard parts in e.Pe and remember them in
772//   * e.hard-parts.
773//   */
774//  e.Pe : t.l e.right,
775//  () (t.l) (e.right) <Cyclic e.right> $iter {
776//    e.cyclic : t.var e.rest,
777//      e.right : e.new-hard t.var e.new-right, {
778//        e.new-hard : v =
779//          (e.hard-parts
780//            ((e.left) e.new-hard (t.var e.new-right))
781//          ) (e.left e.new-hard t.var) (e.new-right) e.rest;
782//        (e.hard-parts) (e.left t.var) (e.new-right) e.rest;
783//      };
784//  } :: (e.hard-parts) (e.left) (e.right) e.cyclic,
785//  e.cyclic : /*empty*/ =
786////  <WriteLN Hard-parts e.hard-parts>,
787//  /*
788//   * For each hard part (or until some variables ranges are
789//   * changed or some inequalitys are added) try to match it with
790//   * corresponding part of e.Re.
791//   */
792//  (e.hard-parts)
793//  (e1 (e.Re) (s.dir e.Pe)) (e2) e.Snt $iter {
794//    e.hard-parts : ((e.left-i) e.hard-i (e.right-i)) e.rest,
795//      <Cyclic e.left-i> :: e.cyc-left,
796//      <Hard e.left-i> :: e.hard-left,
797//      <Reverse <Cyclic e.right-i>> :: e.cyc-right,
798//      <Hard e.right-i> :: e.hard-right,
799//      <Min-Length e.hard-left> :: s.left-len,
800//      <Min-Length e.hard-right> :: s.right-len,
801//      <"+" <Get-Min e.cyc-left> s.left-len> :: s.left-min,
802//      <Get-Max e.cyc-left> : s.left-max,
803//      <"+" s.left-max s.left-len> :: s.left-max,
804//      <"+" <Get-Min e.cyc-right> s.right-len> :: s.right-min,
805//      <Get-Max e.cyc-right> : s.right-max,
806//      <"+" s.right-max s.right-len> :: s.right-max,
807//      <Min-Length e.hard-i> :: s.hard-len,
808//      <Min-Length e.Re> :: s.len,
809//      <"-" s.len <"+" s.right-max s.hard-len>> :: s.left,
810//      <"-" s.len <"+" s.left-max s.hard-len>> :: s.right,
811//      <WriteLN Hard e.hard-i>,
812//      <WriteLN Hard-len s.hard-len>,
813//      <WriteLN Left-len s.left-len>,
814//      <WriteLN Right-len s.right-len>,
815//      <WriteLN Len s.len>,
816//      <WriteLN Left s.left>,
817//      <WriteLN Left-min s.left-min>,
818//      <WriteLN Left-max s.left-max>,
819//      <WriteLN Right s.right>,
820//      <WriteLN Right-min s.right-min>,
821//      <WriteLN Right-max s.right-max>,
822//      {
823//        s.left-min : s.left, s.right-min : s.right =
824//          <Middle-Exp s.left s.right e.Re> :: (e.middle) e.change,
825//          <WriteLN Middle-Exp e.middle>,
826//          <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
827//          <Match-Exp (e.middle) e.hard-i> :: s.new-left s.new-right,
828//          <WriteLN Match-Exp s.new-left s.new-right>,
829//          {
830//            s.new-left : 0, s.new-right : 0 =
831//              (e.rest) (e1) (e2) e.Snt;
832//            /*
833//             * If founded matchings are coinsided then split our
834//             * clash into three new ones.
835//             */
836//            <"+" s.hard-len <"+" s.new-left s.new-right>>
837//            : s.len =
838//              <"+" s.left s.new-left> :: s.left,
839//              <"+" s.right s.new-right> :: s.right,
840//              <Left-Exp s.left s.hard-len e.Re> :: (e.left-Re) e.change,
841//              <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
842//              Unwatched (e.left-Re) (s.dir e.hard-i) :: e.new-hard,
843//              <Left-Exp 0 s.left e.Re> :: (e.left-Re) e.change,
844//              <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
845//              Unwatched (e.left-Re) (s.dir e.left-i) :: e.new-left,
846//              <Right-Exp 0 s.right e.Re> :: (e.right-Re) e.change,
847//              <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
848//              Unwatched (e.right-Re) (s.dir e.right-i) :: e.new-right,
849//              s.dir : {
850//                LEFT =
851//                  e.new-hard e.new-left e.new-right;
852//                RIGHT =
853//                  e.new-hard e.new-right e.new-left;
854//              } :: e.new-clashes,
855//              e1 : e1-new t t,
856//              () (e1-new e.new-clashes) (e2) e.Snt;
857//            /*
858//             * Else we've got some new inequalites...
859//             */
860//            =
861//              <"+" s.left <"-" s.new-left s.left-len>> :: s.num,
862//              <WriteLN NUM s.num>,
863//              <Add-Greater-Ineq (e.cyc-left s.num) (e1) (e2) e.Snt>
864//                :: (e1) (e2) e.Snt,
865//              <"+" s.right <"-" s.new-right s.right-len>> :: s.num,
866//              <WriteLN NUM s.num>,
867//              <Add-Greater-Ineq (e.cyc-right s.num) (e1) (e2) e.Snt>
868//                :: (e1) (e2) e.Snt,
869//              <"-" s.len <"+" s.right <"+" s.new-right
870//                <"+" s.hard-len s.left-len>>>> :: s.num,
871//              <WriteLN NUM s.num>,
872//              <Add-Less-Ineq (e.cyc-left s.num) (e1) (e2) e.Snt>
873//                :: (e1) (e2) e.Snt,
874//              <"-" s.len <"+" s.left <"+" s.new-left
875//                <"+" s.hard-len s.right-len>>>> :: s.num,
876//              <WriteLN NUM s.num>,
877//              <Add-Less-Ineq (e.cyc-right s.num) (e1) (e2) e.Snt>
878//                :: (e1) (e2) e.Snt,
879//              (e.rest) (e1) (e2) e.Snt;
880//          };
881//        /*
882//         * At least one inequlity shurely will be added, so we'll go
883//         * out of the $iter.
884//         */
885//        = {
886//          <"<" (s.left-min) (s.left)> =
887//            <Add-Greater-Ineq (e.cyc-left s.left) (e1) (e2) e.Snt>;
888//          (e1) (e2) e.Snt;
889//        } :: (e1) (e2) e.Snt, {
890//          <">" (s.left-min) (s.left)> =
891//            <"-" s.len <"+" s.left-min <"+" s.hard-len s.right-len>>>
892//              :: s.left,
893//            <Add-Less-Ineq (e.cyc-right s.left) (e1) (e2) e.Snt>;
894//          (e1) (e2) e.Snt;
895//        } :: (e1) (e2) e.Snt, {
896//          <"<" (s.right-min) (s.right)> =
897//            <Add-Greater-Ineq (e.cyc-right s.right) (e1) (e2) e.Snt>;
898//          (e1) (e2) e.Snt;
899//        } :: (e1) (e2) e.Snt, {
900//          <">" (s.right-min) (s.right)> =
901//            <"-" s.len <"+" s.right-min <"+" s.hard-len s.left-len>>>
902//              :: s.right,
903//            <Add-Less-Ineq (e.cyc-left s.right) (e1) (e2) e.Snt>;
904//          (e1) (e2) e.Snt;
905//        } :: (e1) (e2) e.Snt,
906//          () (e1) (e2) e.Snt;
907//      };
908//  } :: (e.hard-parts) (e1) (e2) e.Snt,
909//  \{
910//    e1 : \{ e Unwatched (e) (e); e Unwatched Hard (e) (e); };
911//    e.hard-parts : /*empty*/;
912//  } =
913//  e1 e2 (e.Snt);
914//
915///*
916// * If occurrence of e.Pe is found in e.Re and it can be there then return
917// * variables which should be minimized.
918// * If found occurence of e.Re isn't legal then return empty expression.
919// * And return $fail if there are no occurences of e.Re in e.Pe.
920// */
921//Self-Occur (e.Re) e.Pe, <WriteLN Occur (e.Re) e.Pe>, {
922//  e.Re : e1 e.Pe e2 , {
923//    <Min-Length e1 e2> : 0 = Occur e1 e2;
924//    /*empty*/;
925//  };
926//  e.Pe Not-Found $iter {
927//    e.Pe : e (PAREN v.pe-expr) e, {
928//      e.Re : e v.pe-expr e = Found;
929//      v.pe-expr Not-Found;
930//    };
931//  } :: e.Pe s.found?,
932//  \{
933//    s.found? : Found = /*empty*/;
934//    # \{ e.Pe : e (PAREN v) e; } = $fail;
935//  };
936//};
937//
938//Cyclic e.expr =
939//  () e.expr $iter {
940//    e.expr : t1 e2, t1 : {
941//      s.ObjectSymbol = /*empty*/;
942////      (REF t.name) = ???
943//      (PAREN e) = /*empty*/;
944//      (s.var-tag s.m (e.n) e.var-id), # \{ s.m : e.n; } = t1;
945//      t = /*empty*/;
946//    } :: e.new-cyclic,
947//    (e.cyclic e.new-cyclic) e2;
948//  } :: (e.cyclic) e.expr,
949//  e.expr : /*empty*/ =
950//  e.cyclic;
951//
952//Hard e.expr =
953//  () e.expr $iter {
954//    e.expr : t1 e2, t1 : {
955//      s.ObjectSymbol = t1;
956////      (REF t.name) = ???
957//      (PAREN e) = t1;
958//      (s.var-tag s.m (e.n) e.var-id), # \{ s.m : e.n; } = /*empty*/;
959//      t = t1;
960//    } :: e.new-hard,
961//    (e.hard e.new-hard) e2;
962//  } :: (e.hard) e.expr,
963//  e.expr : /*empty*/ =
964//  e.hard;
965//
966////Hard-Exp? e.expr =
967////  e.expr () $iter \{
968////    <Cyclic e.expr> () $iter {
969////      e.cyclic : (s.tag t t e.var-id) e.rest, {
970////        <Known-Vars? (s.tag e.var-id)> = e.rest (e.num);
971////        e.rest (e.num I);
972////      };
973////    } :: e.cyclic (e.num),
974////      <WriteLN Hard-Exp e.cyclic (e.num)>,
975////      \{
976////        e.num : I I = $fail;
977////        e.cyclic : /*empty*/, {
978////          e.expr : e1 (PAREN e.paren) e2 = e.paren (e.watched e2);
979////          e.watched : e1 (PAREN e.paren) e2 = e.paren (e2);
980////          /*empty*/ ();
981////        };
982////      };
983////  } :: e.expr (e.watched),
984////  e.expr : /*empty*/;
985//
986//Exchange (e.var-holder) (e.new-expr) e.clashes (e.Snt) =
987//  e.var-holder : t.var,
988//  /*
989//   * Mark containing t.var clashes as "Unwatched" and change t.var to
990//   * t.new-var in them.
991//   */
992//  () e.clashes $iter {
993//    e.clashes : e.tag (e.Re) (e.Pe) e.rest,
994//      {
995//        e.tag : Watched = Watched;
996//        Unwatched;
997//      } :: s.watched?,
998//      {
999//        <Vars e.Re> <Vars e.Pe> : e t.var e =
1000//          (e.new-clashes
1001//          s.watched? <Subst (t.var) ((e.new-expr)) (e.Re) (e.Pe)>
1002//          ) e.rest;
1003//        (e.new-clashes e.tag (e.Re) (e.Pe)) e.rest;
1004//      };
1005//  } :: (e.new-clashes) e.clashes,
1006//  e.clashes : /*empty*/ =
1007//  /*
1008//   * Remove all inequalitys wich contain t.var.
1009//   */
1010//  () <? &Greater-Ineqs> $iter {
1011//    e.ineqs : t.ineq e.rest,
1012//      {
1013//        t.ineq : (e t.var e) = /*empty*/;
1014//        t.ineq;
1015//      } :: e.ineq,
1016//      (e.new-ineqs e.ineq) e.rest;
1017//  } :: (e.new-ineqs) e.ineqs,
1018//  e.ineqs : /*empty*/ =
1019//  <Store &Greater-Ineqs e.new-ineqs>,
1020//  () <? &Less-Ineqs> $iter {
1021//    e.ineqs : t.ineq e.rest,
1022//      {
1023//        t.ineq : (e t.var e) = /*empty*/;
1024//        t.ineq;
1025//      } :: e.ineq,
1026//      (e.new-ineqs e.ineq) e.rest;
1027//  } :: (e.new-ineqs) e.ineqs,
1028//  e.ineqs : /*empty*/ =
1029//  <Store &Less-Ineqs e.new-ineqs>,
1030//  /*
1031//   * Rename t.var in the rest of current sentence.
1032//   */
1033//  t.var : (s.tag t t e.var-id),     // temporary step
1034////  <Old-Vars e.new-expr> :: e.new-expr,  // temporary step
1035//  e.new-clashes (<Subst ((s.tag e.var-id)) ((e.new-expr)) e.Snt>);
1036//
1037//Exchange-Exp (e.change) (e1) (e2) e.Snt =
1038//{
1039//  e.change : t.old-1 t.new-1 t.new-2 e.change1 =
1040//    <Exchange (t.old-1) (t.new-1 t.new-2) e1 ()> :: e1 t,
1041//    <Exchange (t.old-1) (t.new-1 t.new-2) e2 (e.Snt)> :: e2 (e.Snt),
1042//    {
1043//      e.change1 : t.old-2 e.new-3 =
1044//        <Exchange (t.old-2) (e.new-3) e1 ()> :: e1 t,
1045//        <Exchange (t.old-2) (e.new-3) e2 (e.Snt)> :: e2 (e.Snt),
1046//        (e1) (e2) e.Snt;
1047//      (e1) (e2) e.Snt;
1048//    };
1049//  (e1) (e2) e.Snt;
1050//};
1051//
1052//Minimize (e.expr) (e.clashes) e.Snt =
1053//  (e.expr) () e.clashes (e.Snt) $iter {
1054//    e.expr : t.var e.rest,
1055//      t.var : (s.tag t t e.var-id),
1056//      {
1057//        <Known-Vars? (s.tag e.var-id)> = (t.var 0);
1058//        /*empty*/;
1059//      } :: e.new-less,
1060//      (e.rest) (e.less e.new-less) <Exchange (t.var) () e.clashes (e.Snt)>;
1061//  } :: (e.expr) (e.less) e.clashes (e.Snt),
1062//  e.expr : /*empty*/ =
1063//  (e.clashes) (e.less) e.Snt;
1064//
1065//Intersect s.k (e.l) s.m (e.n) =
1066//  {
1067//    <"<" (s.k) (s.m)> = s.m;
1068//    s.k;
1069//  } :: s.x,
1070//  {
1071//    e.l e.n : /*empty*/ = /*empty*/;
1072//    e.l : /*empty*/ = e.n;
1073//    e.n : /*empty*/ = e.l;
1074//    <"<" (e.n) (e.l)> = e.n;
1075//    e.l;
1076//  } :: e.y,
1077//  \{
1078//    e.y : /*empty*/ = s.x ();
1079//    <"<=" (s.x) (e.y)> = s.x (e.y);
1080//  };
1081//
1082//Min-Length e.expr =
1083//  0 e.expr $iter {
1084//    e.expr : t1 e2, t1 : {
1085//      s.ObjectSymbol = <"+" s.len 1>;
1086////      (REF t.name) = ???
1087//      (PAREN e) = <"+" s.len 1>;
1088//      (s.var-tag s.m (e.n) e.var-id) = <"+" s.len s.m>;
1089//    } :: s.len,
1090//    s.len e2;
1091//  } :: s.len e.expr,
1092//  e.expr : /*empty*/ =
1093//  s.len;
1094//
1095//Max-Length e.expr =
1096//  0 e.expr $iter {
1097//    e.expr : t1 e2, t1 : {
1098//      s.ObjectSymbol = <"+" s.len 1>;
1099////      (REF t.name) = ???
1100//      (PAREN e) = <"+" s.len 1>;
1101//      (s.var-tag s.m (s.n) e.var-id) = <"+" s.len s.n>;
1102//      (s.var-tag s.m () e.var-id) = Empty;
1103//    } :: s.len,
1104//    s.len e2;
1105//  } :: s.len e.expr,
1106//  \{
1107//    s.len : Empty = /*empty*/;
1108//    e.expr : /*empty*/ = s.len;
1109//  };
1110//
1111//Add-Less-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt =
1112//  <Get-Min e.vars> :: s.min, {
1113//    <">" (s.min) (s.len)> = $fail;
1114//    <Mults e.vars> :: e.mults,
1115//      <Min-Length e.vars> :: s.min-len,
1116//      /*
1117//       * For each variable form new inequality recompute its maximum:
1118//       *  new_max = (s.len - s.min-len + s.mult * min) / s.mult
1119//       */
1120//      () e.vars $iter {
1121//        e.tmp-vars : (s.tag s.m (e.n) e.var-id) e.rest,
1122//          e.mults : e (s.tag s.m (e.n) e.var-id) s.mult e,
1123//          <Div <"+" <"-" s.len s.min-len> <"*" s.mult s.m>> s.mult>
1124//            :: s.max,
1125//          {
1126//            e.n : /*empty*/ = s.max;
1127//            <"<" (e.n) (s.max)> = e.n;
1128//            s.max;
1129//          } :: e.max,
1130//          (e.new-vars (s.tag s.m (e.max) e.var-id)) e.rest;
1131//      } :: (e.new-vars) e.tmp-vars,
1132//      e.tmp-vars : /*empty*/ =
1133//      <Max-Length e.new-vars> : s.max-len, {
1134//        /*
1135//         * Check that maximums weren't decreased too much.
1136//         */
1137//        <">" (s.min) (s.max-len)> = $fail;
1138//        /*
1139//         * If max-len == <<minimal valid value>> then change all
1140//         * e*[min,max] to e*[max,max]. If max == 0 then change variable
1141//         * to empty expression.
1142//         */
1143//        s.min : s.max-len =
1144//          e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
1145//            e.vars : t.var e.rest,
1146//              e.new-vars : (s.tag s.m (s.n) e.var-id) e.new-rest, {
1147//                s.n : 0 =
1148////                  <Exchange (t.var) () e.clashes1 ()>
1149////                    :: e.clashes1 t,
1150////                  <Exchange (t.var) () e.clashes2 (e.Snt)>
1151////                    :: e.clashes2 (e.Snt),
1152//                  e.rest (e.new-rest)
1153//                  (e.clashes1 Unwatched (t.var) (LEFT))
1154//                  (e.clashes2) (e.Snt);
1155//                <Exchange (t.var) ((s.tag s.n (s.n) e.var-id))
1156//                  e.clashes1 ()> :: e.clashes1 t,
1157//                  <Exchange (t.var) ((s.tag s.n (s.n) e.var-id))
1158//                    e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
1159//                  e.rest (e.new-rest) (e.clashes1)
1160//                    (e.clashes2) (e.Snt);
1161//              };
1162//          } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
1163//          e.vars : /*empty*/ =
1164//          (e.clashes1) (e.clashes2) e.Snt;
1165//        /*
1166//         * If no maximums were changed then see whether we should add
1167//         * new inequality to storage and if so then mark clashes
1168//         * containing e.vars in the begining or reversed e.vars in the
1169//         * end as "Unwatched Hard".
1170//         */
1171//        e.vars : e.new-vars, {
1172//          <">" (<Get-Max e.vars>) (s.len)>,
1173//            () <? &Less-Ineqs> $iter e.tmp-ineqs : {
1174//              e1 (e.vars e.ineq s.in-len) e2,
1175//                <Max-Length e.ineq> : s.ineq-max,
1176//                <"<=" (<"+" s.len s.ineq-max>) (s.in-len)>,
1177//                (e.ineqs e1) e2;
1178//              e1 = (e.ineqs e1);
1179//            } :: (e.ineqs) e.tmp-ineqs,
1180//            e.tmp-ineqs : /*empty*/ =
1181//            {
1182//              e.ineqs : e1 (e.vars e.ineq) e2 =
1183//                e1 (e.vars s.len) (e.vars e.ineq) e2;
1184//              e.ineqs (e.vars s.len);
1185//            } :: e.ineqs,
1186//            <Store &Less-Ineqs e.ineqs>,
1187//            (<Mark-Unw-Hard (e.vars) e.clashes1>)
1188//            (<Mark-Unw-Hard (e.vars) e.clashes2>)
1189//            e.Snt;
1190//          (e.clashes1) (e.clashes2) e.Snt;
1191//        };
1192//        /*
1193//         * Else, if some maximums were changed, then change them in all
1194//         * clashes and in Snt. For each variable maximum can't be less
1195//         * then minimum because it would mean that s.len < s.min.
1196//         * If max == 0 then change variable to empty expression.
1197//         */
1198//        e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
1199//          e.vars : t.var e.rest,
1200//            e.new-vars : (s.tag s.m (s.n) e.var-id) e.new-rest, {
1201//              t.var : (s.tag s.m (s.n) e.var-id) =
1202//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
1203//              s.n : 0 =
1204////                <Exchange (t.var) () e.clashes1 ()>
1205////                  :: e.clashes1 t,
1206////                <Exchange (t.var) () e.clashes2 (e.Snt)>
1207////                  :: e.clashes2 (e.Snt),
1208//                e.rest (e.new-rest)
1209//                (e.clashes1 Unwatched (t.var) (LEFT)) (e.clashes2)
1210//                (e.Snt);
1211//              <Exchange (t.var) ((s.tag s.m (s.n) e.var-id))
1212//                e.clashes1 ()> :: e.clashes1 t,
1213//                <Exchange (t.var) ((s.tag s.m (s.n) e.var-id))
1214//                  e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
1215//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
1216//            };
1217//        } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
1218//        e.vars : /*empty*/ =
1219//        (e.clashes1) (e.clashes2) e.Snt;
1220//      };
1221//  };
1222//
1223//Add-Greater-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt, {
1224//  <Get-Max e.vars> : s.max, {
1225//    <"<" (s.max) (s.len)> = $fail;
1226//    <Mults e.vars> :: e.mults,
1227//      <Max-Length e.vars> : s.max-len,
1228//      /*
1229//       * For each variable from new inequality recompute its minimum:
1230//       *  new_min = ceil ((s.len - s.max-len + s.mult * max) / s.mult)
1231//       */
1232//      () e.vars $iter {
1233//        e.tmp-vars : (s.tag s.m (s.n) e.var-id) e.rest,
1234//          e.mults : e (s.tag s.m (s.n) e.var-id) s.mult e,
1235//          <Ceil <"+" <"-" s.len s.max-len> <"*" s.mult s.n>> s.mult>
1236//            :: s.min,
1237//          {
1238//            <"<" (s.min) (0)> = 0;
1239//            <">" (s.m) (s.min)> = s.m;
1240//            s.min;
1241//          } :: s.min,
1242//          (e.new-vars (s.tag s.min (s.n) e.var-id)) e.rest;
1243//      } :: (e.new-vars) e.tmp-vars,
1244//      e.tmp-vars : /*empty*/ =
1245//      <Min-Length e.new-vars> :: s.min-len, {
1246//        /*
1247//         * Check that minimums weren't increased too much.
1248//         */
1249//        <"<" (s.max) (s.min-len)> = $fail;
1250//        /*
1251//         * If min-len == <<maximum valid value>> then change all
1252//         * e*[min,max] to e*[min,min].
1253//         */
1254//        s.max : s.min-len =
1255//          e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
1256//            e.vars : t.var e.rest,
1257//              e.new-vars : (s.tag s.m (s.n) e.var-id) e.new-rest,
1258//              <Exchange (t.var) ((s.tag s.m (s.m) e.var-id))
1259//                e.clashes1 ()> :: e.clashes1 t,
1260//              <Exchange (t.var) ((s.tag s.m (s.m) e.var-id))
1261//                e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
1262//              e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
1263//          } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
1264//          e.vars : /*empty*/ =
1265//          (e.clashes1) (e.clashes2) e.Snt;
1266//        /*
1267//         * If no minimums were changed then see whether we should add
1268//         * new inequality to storage and if so then mark clashes
1269//         * containing e.vars in the begining or reversed e.vars in the
1270//         * end as "Unwatched Hard".
1271//         */
1272//        e.vars : e.new-vars, {
1273//          <"<" (<Get-Min e.vars>) (s.len)>,
1274//            () <? &Greater-Ineqs> $iter e.tmp-ineqs : {
1275//              e1 (e.vars e.ineq s.in-len) e2,
1276//                <">=" (<"+" s.len <Min-Length e.ineq>>) (s.in-len)>,
1277//                (e.ineqs e1) e2;
1278//              e1 = (e.ineqs e1);
1279//            } :: (e.ineqs) e.tmp-ineqs,
1280//            e.tmp-ineqs : /*empty*/ =
1281//            {
1282//              e.ineqs : e1 (e.vars e.ineq) e2 =
1283//                e1 (e.vars s.len) (e.vars e.ineq) e2;
1284//              e.ineqs (e.vars s.len);
1285//            } :: e.ineqs,
1286//            <Store &Greater-Ineqs e.ineqs>,
1287//            (<Mark-Unw-Hard (e.vars) e.clashes1>)
1288//            (<Mark-Unw-Hard (e.vars) e.clashes2>)
1289//            e.Snt;
1290//          (e.clashes1) (e.clashes2) e.Snt;
1291//        };
1292//        /*
1293//         * Else, if some minimums were changed, then change them in all
1294//         * clashes and in Snt. For each variable minimum can't be greater
1295//         * then maximum because it would mean that s.len > s.max.
1296//         */
1297//        e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
1298//          e.vars : t.var e.rest,
1299//            e.new-vars : t.new-var e.new-rest, {
1300//              t.var : t.new-var =
1301//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
1302//              <Exchange (t.var) (t.new-var) e.clashes1 ()>
1303//                :: e.clashes1 t,
1304//                <Exchange (t.var) (t.new-var) e.clashes2 (e.Snt)>
1305//                  :: e.clashes2 (e.Snt),
1306//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
1307//            };
1308//        } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
1309//        e.vars : /*empty*/ =
1310//        (e.clashes1) (e.clashes2) e.Snt;
1311//      };
1312//  };
1313//  e.vars : (s.tag s.n () e.var-id), {
1314//    <">" (s.len) (s.n)> =
1315//      <Exchange ((s.tag s.n () e.var-id)) ((s.tag s.len () e.var-id))
1316//        e.clashes1 ()> :: e.clashes1 t,
1317//      <Exchange ((s.tag s.n () e.var-id)) ((s.tag s.len () e.var-id))
1318//        e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
1319//      (e.clashes1) (e.clashes2) e.Snt;
1320//    (e.clashes1) (e.clashes2) e.Snt;
1321//  };
1322//  (e.clashes1) (e.clashes2) e.Snt;  // STUB!!! Add inequality to the storage?
1323//};
1324//
1325//Get-Min e.vars, {
1326//  <? &Greater-Ineqs> : $r e (e.ineq s.len) e,
1327//    e.vars : e.ineq e.other,
1328//    <"+" s.len <Min-Length e.other>>;
1329//  <Min-Length e.vars>;
1330//};
1331//
1332//Get-Max e.vars, {
1333//  <? &Less-Ineqs> : $r e (e.ineq s.len) e,
1334//    e.vars : e.ineq e.other,
1335//    <Max-Length e.other> : s.other-len,
1336//    <"+" s.len s.other-len>;
1337//  <Max-Length e.vars>;
1338//};
1339//
1340///*
1341// * Computes variables multiplicitys and returns them in the form:
1342// *  e.mults ::= t.var s.mult e.mults | []
1343// */
1344//Mults e.vars =
1345//  () e.vars $iter {
1346//    e.vars : t.var e.rest,
1347//      1 e.rest $iter {
1348//        e.rest : e1 t.var e2,
1349//          <"+" s.mult 1> e1 e2;
1350//      } :: s.mult e.rest,
1351//      # \{ e.rest : e t.var e; } =
1352//      (e.mults t.var s.mult) e.rest;
1353//  } :: (e.mults) e.vars,
1354//  e.vars : /*empty*/ =
1355//  e.mults;
1356//
1357//Mark-Unw-Hard (e.vars) e.clashes =
1358//  <Reverse e.vars> :: e.rev-vars,
1359//  () e.clashes $iter e.clashes : {
1360//    (e.Re) (e.Pe) e.rest,
1361//      <Cyclic e.Re> :: e.cyc-Re,
1362//      <Cyclic e.Pe> :: e.cyc-Pe,
1363//      {
1364//        \{
1365//          e.cyc-Re : e.vars e;
1366//          e.cyc-Re : e e.rev-vars;
1367//          e.cyc-Pe : e.vars e;
1368//          e.cyc-Pe : e e.rev-vars;
1369//        },
1370//          (e.new-clashes Unwatched Hard (e.Re) (e.Pe)) e.rest;
1371//        (e.new-clashes (e.Re) (e.Pe)) e.rest;
1372//      };
1373//    e.tag (e.Re) (e.Pe) e.rest =
1374//      (e.new-clashes e.tag (e.Re) (e.Pe)) e.rest;
1375//  } :: (e.new-clashes) e.clashes,
1376//  e.clashes : /*empty*/ =
1377//  e.new-clashes;
1378//
1379//Ceil s1 s2, {
1380//  <Rem s1 s2> : 0 = <Div s1 s2>;
1381//  <"+" <Div s1 s2> 1>;
1382//};
1383//
1384//Match-Exp (e.Re) e.Pe =
1385//  <Granulate e.Re> :: e.Re,
1386//  <Granulate e.Pe> :: e.Pe,
1387//  <Length e.Pe> :: s.len,
1388//  e.Re : e1 e2,
1389//  <Match (<Left 0 s.len e2>) (e.Pe)>,
1390//  e2 : $r e3 e4,
1391//  <Match (<Right 0 s.len e3>) (e.Pe)>,
1392//  <Length e1> <Length e4>;
1393//
1394//Match e.clash =
1395//  e.clash $iter e.clashes : \{
1396//    e1 (e.expr) (e.expr) e2 = e1 e2;
1397//    e1 (t.Rt e.Re) (t.Pt e.Pe) e2,
1398//      # \{ t.Rt : (EVAR e); t.Pt : (EVAR e); } =
1399//      <Match-Term t.Rt t.Pt e1 (e.Re) (e.Pe) e2>;
1400//    e1 (e.Re t.Rt) (e.Pe t.Pt) e2,
1401//      # \{ t.Rt : (EVAR e); t.Pt : (EVAR e); } =
1402//      <Match-Term t.Rt t.Pt e1 (e.Re) (e.Pe) e2>;
1403//    e1 (e.Re) (e.Pe) e2, \{
1404//      e.Re : (EVAR e) e (EVAR e) = <Match-Cyclic (e.Re) (e.Pe) e1 e2>;
1405//      e.Pe : (EVAR e) e (EVAR e) = <Match-Cyclic (e.Pe) (e.Re) e1 e2>;
1406//      \{
1407//        e.Re : (EVAR e) e, e.Pe : e (EVAR e);
1408//        e.Re : (EVAR e) e, e.Pe : e (EVAR e);
1409//      } =
1410//        <Intersect <Min-Length e.Re> (<Max-Length e.Re>)
1411//          <Min-Length e.Pe> (<Max-Length e.Pe>)>; // This is STUB!!!
1412//    };
1413//  } :: e.clashes,
1414//  <WriteLN Match e.clashes>,
1415//  e.clashes : /*empty*/;
1416//
1417//Match-Term {
1418//  term term e.clashes = e.clashes;
1419//  t.Rt t.Pt e.clashes, t.Rt : {
1420//    s.ObjectSymbol =
1421//      t.Pt : (s.tag e),
1422//      SVAR TVAR : e s.tag e,  // check that s.tag isn't PAREN
1423//      <Subst (t.Pt) ((t.Rt)) e.clashes>;
1424//    (SVAR e), t.Pt : {
1425//      s.ObjectSymbol = <Subst (t.Rt) ((t.Pt)) e.clashes>;
1426//      (s.tag e) =
1427//        SVAR TVAR : e s.tag e,  // check that s.tag isn't PAREN
1428//        <Subst (t.Pt) ((t.Rt)) e.clashes>;
1429//    };
1430//    (TVAR e) =
1431//      <Subst (t.Rt) ((t.Pt)) e.clashes>;
1432//    (PAREN e.Re) = t.Pt : \{
1433//      (TVAR e) = <Subst (t.Pt) ((t.Rt)) e.clashes>;
1434//      (PAREN e.Pe) = (e.Re) (e.Pe) e.clashes;
1435//    };
1436//  };
1437//};
1438//
1439//Match-Cyclic (e.Re) (e.Pe) e.clashes = ;  // This is STUB!!!
1440//
1441//Granulate e.expr =
1442//  (e.expr) <Vars e.expr> $iter {
1443//    e.vars : t.var e.rest,
1444//      t.var : {
1445//        (s.tag 1 (1) e.var-id), {
1446//          SVAR TVAR : e s.tag e = e.expr;
1447//          <Subst (t.var) (((TVAR 1 (1)) e.var-id)) e.expr>;
1448//        };
1449//        (s.tag s.n (s.n) e.NEW (e.QualifiedName)) =
1450//          s.n /*empty*/ $iter
1451//            <"-" s.n 1>
1452//            (TVAR 1 (1) NEW ("gran" e.QualifiedName s.n)) e.new-vars
1453//          :: s.n e.new-vars,
1454//          s.n : 0 =
1455//          <Subst (t.var) ((e.new-vars)) e.expr>;
1456//        (s.tag e.something), {  // cyclic variable
1457//          s.tag : EVAR = e.expr;
1458//          <Subst (t.var) (((EVAR e.something))) e.expr>;
1459//        };
1460//      } :: e.expr,
1461//      (e.expr) e.rest;
1462//  } :: (e.expr) e.vars,
1463//  e.vars : /*empty*/ =
1464//  e.expr;
1465//
1466//Left-Exp s.left s.len e.expr, \{
1467//  <"<" (<Min-Length e.expr>) (<"+" s.left s.len>)>
1468//    = $fail;
1469//  s.len : 0 = ();
1470//  s.left : 0 =
1471//    0 () e.expr $iter \{
1472//      e.expr : t1 e2, t1 : {
1473//        s.ObjectSymbol = <"+" s.num 1>;
1474////        (REF t.name) = ???
1475//        (PAREN e) = <"+" s.num 1> ;
1476//        (s.var-tag s.n (s.n) e.var-id) = <"+" s.num s.n>;
1477//        (s.var-tag s.m (e.n) e.var-id) =
1478//          <"+" s.num s.m> :: s.num,
1479//          <"<=" (s.len) (s.num)>,
1480//          s.num;
1481//      } :: s.num,
1482//        s.num (e.left t1) e2;
1483//    } :: s.num (e.left) e.expr,
1484//    <"<=" (s.len) (s.num)> =
1485//    <"-" s.num s.len> :: s.r-min,
1486//    e.left : e.first t.var,
1487//    t.var : {
1488//      s.ObjectSymbol = (e.left);
1489//      (PAREN e) = (e.left);
1490//      (s.tag s.m (e.n) e.NEW (e.QualifiedName)) =
1491//        <"-" s.m s.r-min> :: s.l-len,
1492//        e.n : {
1493//          /*empty*/ = /*empty*/;
1494//          s.x = <"-" <"+" s.x <Min-Length e.first>> s.l-len>;
1495//        } : {
1496//          0 = (e.left);
1497//          e.r-max,
1498//            (s.tag s.l-len (s.l-len) NEW ("l-split" e.QualifiedName))
1499//              :: t.l-var,
1500//            (s.tag s.r-min (e.r-max) NEW ("r-split" e.QualifiedName))
1501//              :: t.r-var,
1502//            <Subst (t.var) ((t.l-var t.r-var)) e.first> :: e.expr,
1503//            (e.expr t.l-var) t.var t.l-var t.r-var;
1504//        };
1505//    };
1506//  <Left-Exp 0 s.left e.expr> :: (e.left) e.change,
1507//    {
1508//      e.change : t.old-var t.new-1 t.new-2 =
1509//        <Subst (t.old-var) ((t.new-1 t.new-2)) e.expr>;
1510//      e.expr;
1511//    } : e.left e.right,
1512//    <Left-Exp 0 s.len e.right> e.change;
1513//};
1514//
1515//Right-Exp s.right s.len e.expr, \{
1516//  <"<" (<Min-Length e.expr>) (<"+" s.right s.len>)>
1517//    = $fail;
1518//  s.len : 0 = ();
1519//  s.right : 0 =
1520//    0 () e.expr $iter \{
1521//      e.expr : e2 t1, t1 : {
1522//        s.ObjectSymbol = <"+" s.num 1>;
1523////        (REF t.name) = ???
1524//        (PAREN e) = <"+" s.num 1> ;
1525//        (s.var-tag s.n (s.n) e.var-id) = <"+" s.num s.n>;
1526//        (s.var-tag s.m (e.n) e.var-id) =
1527//          <"+" s.num s.m> :: s.num,
1528//          <"<=" (s.len) (s.num)>,
1529//          s.num;
1530//      } :: s.num,
1531//        s.num (t1 e.right) e2;
1532//    } :: s.num (e.right) e.expr,
1533//    <"<=" (s.len) (s.num)> =
1534//    <"-" s.num s.len> :: s.l-min,
1535//    e.right : t.var e.last,
1536//    t.var : {
1537//      s.ObjectSymbol = (e.right);
1538//      (PAREN e) = (e.right);
1539//      (s.tag s.m (e.n) e.NEW (e.QualifiedName)) =
1540//        <"-" s.m s.l-min> :: s.r-len,
1541//        e.n : {
1542//          /*empty*/ = /*empty*/;
1543//          s.x = <"-" <"+" s.x <Min-Length e.last>> s.r-len>;
1544//        } : {
1545//          0 = (e.right);
1546//          e.l-max,
1547//            (s.tag s.r-len (s.r-len) NEW ("r-split" e.QualifiedName))
1548//              :: t.r-var,
1549//            (s.tag s.l-min (e.l-max) NEW ("l-split" e.QualifiedName))
1550//              :: t.l-var,
1551//            <Subst (t.var) ((t.l-var t.r-var)) e.last> :: e.expr,
1552//            (e.expr t.r-var) t.var t.l-var t.r-var;
1553//        };
1554//    };
1555//  <Right-Exp 0 s.right e.expr> :: (e.right) e.change,
1556//    {
1557//      e.change : t.old-var t.new-1 t.new-2 =
1558//        <Subst (t.old-var) ((t.new-1 t.new-2)) e.expr>;
1559//      e.expr;
1560//    } : e.left e.right,
1561//    <Right-Exp 0 s.len e.left> e.change;
1562//};
1563//
1564////  Right-Exp s.right s.len e.expr =
1565////    <Min-Length e.expr> :: s.expr-len,
1566////    <"+" s.right s.len> :: s.sum,
1567////    \{
1568////      <"<" (s.expr-len) (s.sum)> = $fail;
1569////      <Left-Exp <"-" s.expr-len s.sum> s.len e.expr>;
1570////    };
1571// 
1572//Middle-Exp s.left s.right e.expr, \{
1573//  <"<" (<Min-Length e.expr>) (<"+" s.left s.right>)>
1574//    = $fail;
1575//  <Left-Exp 0 s.left e.expr> :: (e.left) e.l-change,
1576//    <Right-Exp 0 s.right e.expr> :: (e.right) e.r-change,
1577//    e.expr : e.left e.sought e.right,
1578//    (e.sought) e.l-change e.r-change;
1579//};
1580
Note: See TracBrowser for help on using the repository browser.