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

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