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

Last change on this file since 2043 was 2043, checked in by orlov, 14 years ago
  • Improved block extraction from result expressions.
  • Use asail2asail when converting to C++.
  • Remove duplicate declarations after cleanup of blocks

(rfp_asail2asail.Remove-Dupl-Decl).

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