source: to-imperative/trunk/compiler/refal/org/refal/plus/compiler/rfp_as2as.rf @ 3956

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