// $Source$
// $Revision$
// $Date$

$use "rfpc";
$use "rfp_compile";
$use "rfp_format";
$use "rfp_helper";
$use "rfp_vars";
$use "rfp_debug";

$use Arithm Box Class List StdIO Table;

// transform only e.targets and leave all the rest as it is
$func Transform (e.targets) e.Items = e.Items;

// transform { A; } : Pe into { A; } :: aux, aux : Pe
$func Unstick-Blocks e.Sentence = e.Sentence (e.Fe);

// remove blocks from Re
$func Flatten-Result s.tail? (e.Re) e.items = e.assigns (e.Re);

$func Generate-In-Vars (e.in) e.branch = (e.in) e.branch;

// rename variables local for the {}-blocks
//$func Rename-Vars s.num (e.upper-vars) (e.res-vars) e.Snt = e.new-Snt;
$func Rename-Vars e = e;

// is variable with e.QualifiedName in the e.vars list?
//$func? Old-Var? e.vars (s t (e.QualifiedName)) = ;
$func? Old-Var? e = e;

//$func Rename s.num (s.tag t.p (e.QualifiedName)) =
//                      (s.tag t.p ("ren" e.QualifiedName s.num));
$func Rename e = e;

// build substitution for all occurrences of each e.var in e.Snt
$func Build-Subst (e.vars) (e.substs) e.Snt = (e.patterns) (e.replacements);

// build substitution for all occurrences of variable with the name t.n in e.Snt
$func Var-Subst s.var-tag t.n t.s e.Snt = (e.patterns) (e.replacements);

$box Free-Idx;


RFP-As2As-Transform e.Items =
  { <Lookup &RFP-Options ITEMS>;; } :: e.targets,
  <Transform (e.targets) e.Items>;

Transform (e.targets) e.Items, {
  e.Items : t.item e.rest, {
    {
      e.targets : v =
        e.targets : e t.name e,
        t.item : (t t t t.name e);;
    },
      t.item : (s.link s.tag t.pragma t.name (e.in) (e.out) (BRANCH t.p e.branch)) =
      {
        <Format-Exp e.in> : e.in =
          <Generate-In-Vars (e.in) e.branch>;
        (e.in) e.branch;
      } :: (e.in) e.branch,
      {
        <In-Table? &RFP-Options DBG> =
          <Add-Debug (RESULT t.p e.in) e.branch>;
        e.branch;
      } :: e.branch,
      <Store &Free-Idx 1>,
      <Unstick-Blocks e.branch> :: e.branch t,
      <Rename-Vars 0 (<Vars e.in>) () e.branch> :: e.branch,
      (s.link s.tag t.pragma t.name (e.in) (e.out) (BRANCH t.p e.branch));
    t.item;
  } :: t.item =
    t.item <Transform (e.targets) e.rest>;;
};

/*
 * Next function gets use of the following proposition:
 *  one can add (RESULT) term to the end of any sentence that isn't end in
 *  (RESULT e.anything) and it won't change the result of program execution.
 * No, no, the proposition is WRONG!!! Such doings change the semantics of "=".
 * 
 * The function returns the sentence with all { A; } : Pe constructions
 * turned into { A; } :: aux, aux : Pe ones and format of the last Re of
 * the sentence.
 */
Unstick-Blocks e.Sentence, e.Sentence : eL e.Snt, e.Snt : \{
  (s.block t.Pragma e.branches) eR, s.block : \{ BLOCK; BLOCK?; } =
    e.branches () () $iter {
      e.branches : (BRANCH t.p e.branch) e.rest,
        <Unstick-Blocks e.branch> :: e.new-branch (e.Fe),
        e.rest (e.br (BRANCH t.p e.new-branch)) (e.Fes (e.Fe));
    } :: e.branches (e.br) (e.Fes),
    e.branches : /*empty*/ =
    {
      eR : \{
        (BLOCK  t (BRANCH t (LEFT e) e) e) e;
        (BLOCK  t (BRANCH t (RIGHT e) e) e) e;
        (BLOCK? t (BRANCH t (LEFT e) e) e) e;
        (BLOCK? t (BRANCH t (RIGHT e) e) e) e;
        (LEFT e) e;
        (RIGHT e) e;
      } =
        <? &Free-Idx> : s.N,
        <Gener-Var-Indices s.N (<MSG e.Fes>) "aux" "alt"> :: e.aux s.N,
        <Store &Free-Idx s.N>,
        eL (s.block t.Pragma e.br) (FORMAT (PRAGMA) e.aux)
        (RESULT (PRAGMA) e.aux) <Unstick-Blocks eR>;
      eR : /*empty*/ =
        eL (s.block t.Pragma e.br) (<MSG e.Fes>);
      eL (s.block t.Pragma e.br) <Unstick-Blocks eR>;
    };
  (RESULT t.Pragma (s.block e.branches)) eR, s.block : \{ BLOCK; BLOCK?; } =     // FIXME: Comment this and search for BUGs!
    eL <Unstick-Blocks (s.block e.branches) eR>;
  (RESULT t.Pragma e.Re) eR =
    <Flatten-Result Tail () e.Re> :: e.assigns (e.Re),
    {
      e.Re : e1 (FAIL e2) = (RESULT t.Pragma e1) e2;
      (RESULT t.Pragma e.Re);
    } :: e.Result,
    {
      eR : v =
        eL e.assigns e.Result <Unstick-Blocks eR>;
      <Format-Exp e.Re> :: e.Fe,
        <MSG (e.Fe) (e.Fe)> :: e.Fe,  // hack for avoiding non-hard formats
        eL e.assigns e.Result (e.Fe);
    };
  (NOT (BRANCH t.p1 e.body)) eR =
    <Unstick-Blocks e.body> :: e.body t.empty,
    eL (NOT (BRANCH t.p1 e.body)) <Unstick-Blocks eR>;
  (ITER (BRANCH t.p1 e.body) t.IterVars (BRANCH t.p2 e.condition)) =
    <Unstick-Blocks e.body> :: e.body t,
    <Unstick-Blocks e.condition> :: e.condition (e.Format),
    eL (ITER (BRANCH t.p1 e.body) t.IterVars (BRANCH t.p2 e.condition)) (e.Format);
  (TRY (BRANCH t.p1 e.TrySnt) e.NOFAIL t.CatchBlock) =
    <Unstick-Blocks e.TrySnt> :: e.TrySnt t.Try-Fe,
    <Unstick-Blocks t.CatchBlock> :: e.CatchBlock t.Catch-Fe,
    eL (TRY (BRANCH t.p1 e.TrySnt) e.NOFAIL e.CatchBlock) (<MSG t.Try-Fe t.Catch-Fe>);
  (FAIL e) = e.Sentence ((FAIL));
  (ERROR t.Pragma) eR =
    <Unstick-Blocks eR> :: eR t,
    eL (ERROR t.Pragma) eR ((FAIL));
};

Flatten-Result s.tail? (e.Re) e.items, e.items : {
  t1 e.rest, t1 : \{ (BLOCK e); (BLOCK? e); } =
    <Unstick-Blocks t1> :: e1 (e.Format),
    {
      e.Format : (FAIL) =
        (e.Re (FAIL e1));
      <? &Free-Idx> : s.N,
        <Gener-Var-Indices s.N (e.Format) "aux" "block"> :: e.aux s.N,
        <Store &Free-Idx s.N>,
        e1 (FORMAT (PRAGMA) e.aux)
        <Flatten-Result s.tail? (e.Re e.aux) e.rest>;
    };
  (CALL t.p t.name e.r) e.rest =
    <Flatten-Result Not-Tail () e.r> :: e.assigns (e.r),
    (CALL t.p t.name e.r) :: t1,
    {
      e.rest : /*empty*/, s.tail? : Tail =
        e.assigns (e.Re t1);
      <? &Free-Idx> : s.N,
        <Gener-Var-Indices s.N (<Format-Exp t1>) "aux" "call"> :: e.aux1 s.N,
        <Store &Free-Idx s.N>,
        e.assigns (RESULT (PRAGMA) t1) (FORMAT (PRAGMA) e.aux1)
        <Flatten-Result s.tail? (e.Re e.aux1) e.rest>;
    };
  (PAREN e.r) e.rest =
    <Flatten-Result Not-Tail () e.r> :: e.assigns (e.r),
    e.assigns <Flatten-Result s.tail? (e.Re (PAREN e.r)) e.rest>;
  t1 e.rest = <Flatten-Result s.tail? (e.Re t1) e.rest>;
  /*empty*/ = (e.Re);
};


/*
 * Generate variable names for input function parameters. Change e.Sentence so
 * that it doesn't begin with pattern.
 */
Generate-In-Vars (e.in) e.Sentence, {
  /*
   * If input PAlt of a function is a sentence (not a block), format of
   * input pattern coincides t.InputFormat, and all variables in input
   * pattern have different indexes then we can drop the pattern and define
   * function as
   *    func (Fname (pattern_vars) (res_..., res_..., ...)) 
   * where pattern_vars means variables used in the pattern. 
   */
  e.Sentence : \{
    (LEFT t e.Pe) e.Snt = (e.Pe) e.Snt;
    (RIGHT t e.Pe) e.Snt = (e.Pe) e.Snt;
  } :: (e.Pe) e.Snt =
    {
      <Format-Exp e.Pe> : e.in,  // FIXME: here should be checked format equality
        <Vars e.Pe> :: e.args,
        # \{ e.args : e (e t1) e (e t1) e; } =
        (e.Pe) e.Snt;
      <Gener-Var-Indices 1 (e.in) "arg"> :: e.in-expr s =
        (e.in-expr) (RESULT (PRAGMA) e.in-expr) e.Sentence;
    };
  /*
   * Else if we have real PAlt then we can do that transformation with each
   * branch. Input parameters for the function will be arg_1...arg_N. If
   * first pattern in the branch satisfies the conditions then drop it out
   * and rename variables in the branch to arg_1...arg_N instead of pattern
   * variables.
   */
  e.Sentence : (s.block t.Pragma e.branches) e.Snt =
    <Gener-Var-Indices 1 (e.in) "arg"> :: e.in-expr s,
    <Vars e.in-expr> :: e.in-vars,
    (/*e.br*/) e.branches $iter {
      e.branches : (BRANCH t.p (s.dir t.pp e.Pe) e.br-snt) e.rest, {
        <Format-Exp e.Pe> : e.in,  // FIXME: here should be checked format equality
          <Vars e.Pe> :: e.vars,
          # \{ e.vars : e (e t1) e (e t1) e; } =
          <Build-Subst (e.vars) (e.in-vars) e.br-snt> :: (e.pats) (e.repls),
          (e.br (BRANCH t.p <Subst (e.pats) (e.repls) e.br-snt>)) e.rest;
        (e.br (BRANCH t.p (s.dir t.pp e.Pe) e.br-snt)) e.rest;
      };
    } :: (e.br) e.branches,
    e.branches : /*empty*/ =
    (e.in-expr) (s.block t.Pragma e.br) e.Snt;
  /*
   * Else sentence already hasn't begun with pattern, so left it as it is.
   * It can be only if e.in and e.out are both empty.
   */
//!	(e.in) e.Sentence;
} :: (e.in) e.Sentence =
  (e.in) e.Sentence;

/*
 * Each {}-block is seen as inlined function. e.upper-vars and e.res-vars are
 * correspondingly input and output parameters for that function. e.Snt is its
 * body.
 * Rename all variables local for inlined function, for those to be
 * distinguishable from the outer world when the function is inlined in
 * imperative language.
 */
Rename-Vars s.num (e.upper-vars) (e.res-vars) e.Snt =
  (e.upper-vars) (/*e.new-Snt*/) e.Snt $iter {
    e.Snt : t.Statement e.rest, {
      /*
       * If we meet a pattern then add each unknown variable from it to
       * the list and rename local variables which intersect with out
       * parameters of the block.
       */
      t.Statement : \{
        (LEFT t e.Pe) = e.Pe;
        (RIGHT t e.Pe) = e.Pe;
      } :: e.Pe =
        <Split &Old-Var? e.res-vars (<Vars e.Pe>)> :: (e.old-vars) (e.new-vars),
        <Map &Rename s.num (e.old-vars)> :: e.renames,
        <Build-Subst (e.old-vars) (e.renames) e.Snt> :: (e.pats) (e.repls),
        <Subst (e.pats) (e.repls) e.Snt> : (s.tag t.p e.Pe1) e.rest-Snt,
        (<Or (e.vars) <Vars e.Pe1>>) (e.new-Snt (s.tag t.p e.Pe1)) e.rest-Snt;
      /*
       * If we meet format expression then for each already used
       * variable in it select new name by adding prefix "ren".
       */
      t.Statement : (FORMAT t e.He) =
        <Split &Old-Var? e.upper-vars e.res-vars (<Vars e.He>)>
          :: (e.old-vars) (e.new-vars),
        <Map &Rename s.num (e.old-vars)> :: e.renames,
        <Build-Subst (e.old-vars) (e.renames) e.Snt> :: (e.pats) (e.repls),
        <Subst (e.pats) (e.repls) e.Snt> : (FORMAT t.p e.He1) e.rest-Snt,
        (<Or (e.vars) <Vars e.He1>>) (e.new-Snt (FORMAT t.p e.He1)) e.rest-Snt;
      /*
       * We shouldn't rename variable if its duplicate is appeared on
       * a parallel branch of the block. So process all branches
       * iteratively with the same list of variables (known before
       * block).
       */
      t.Statement : (s.block t.Pragma e.branches), s.block : \{ BLOCK; BLOCK?; } =
        /*
         * As well as after-block patterns, formats should be scaned
         * for res-vars.  See samples/Syntax/block1.rf for example.
         */
        e.rest : {
          (LEFT t e.Pe) e = <Vars e.Pe>;
          (RIGHT t e.Pe) e = <Vars e.Pe>;
          (FORMAT t e.He) e = <Vars e.He>;
          /*empty*/ = e.res-vars;
          e = /*empty*/;
        } :: e.bl-res-vars,
        /*
         * Left as res-vars only variables which were unknown before
         * block. Those are local if meet in pattern and need
         * renaming.
         */
        (/*e.brv*/) e.bl-res-vars $iter {
          e.bl-res-vars : e1 (e t.name) e2, e.vars : e (e t.name) e =
            (e.brv e1) e2;
          (e.brv e.bl-res-vars);
        } :: (e.brv) e.bl-res-vars,
        e.bl-res-vars : /*empty*/ =
        <Map &Rename-Vars <"+" s.num 1> (e.vars) (e.brv) (e.branches)>
          :: e.branches,
        (e.vars) (e.new-Snt (s.block t.Pragma e.branches)) e.rest;
      t.Statement : (BRANCH t.Pragma e.Sentence) =
        () (e.new-Snt (BRANCH t.Pragma
            <Rename-Vars s.num (e.vars) (e.res-vars) e.Sentence>));
      t.Statement : (ITER t.IterBody t.IterVars t.IterCondition) =
        <Rename-Vars
          s.num (e.upper-vars) (e.res-vars) t.IterVars t.IterBody
        > : t t.NewBody,
        <Rename-Vars
          s.num (e.upper-vars) (e.res-vars) t.IterVars t.IterCondition
        > :: e.IterCondition,
        () (e.new-Snt (ITER t.NewBody e.IterCondition));
      t.Statement : (TRY t.TryBranch e.NOFAIL t.Catch) =
        <Rename-Vars s.num (e.upper-vars) (e.res-vars) t.TryBranch> :: e.TryBranch,
        <Rename-Vars s.num (e.upper-vars) (e.res-vars) t.Catch> :: e.Catch,
        () (e.new-Snt (TRY e.TryBranch e.NOFAIL e.Catch));
      /*
       * Else proceed with the rest.
       */
      (e.vars) (e.new-Snt t.Statement) e.rest;
    };
  } :: (e.vars) (e.new-Snt) e.Snt,
  e.Snt : /*empty*/ =
  e.new-Snt;

//Old-Var? e.vars (s.tag t (e.QualifiedName)) = e.vars : e (s.tag t (e.QualifiedName)) e;
Old-Var? e.vars (e t.name) = e.vars : e (e t.name) e;

Rename s.num (s.tag t.p (e.QualifiedName)) =
  (s.tag t.p (e.QualifiedName "_" s.num));

/*
 * Build substitution for all occurrences of each e.var in e.Snt.
 */
Build-Subst {
  ((s.tag t t.name) e.vars) ((s t t.s) e.substs) e.Snt =
    <Var-Subst s.tag t.name t.s e.Snt> :: (e.var-pats) (e.var-repls),
    <Build-Subst (e.vars) (e.substs) e.Snt> :: (e.pats) (e.repls),
    (e.var-pats e.pats) (e.var-repls e.repls);
  () () e = () ();
};

/*
 * Build substitution for all occurrences of variable with the name t.n in e.Snt.
 */
Var-Subst s.tag t.n t.s e.Snt, {
  e.Snt : t.Statement e.rest, {
    t.Statement : (s.tag t.p t.name) =
      {
        t.name : t.n = ((s.tag t.p t.name)) (((s.tag t.p t.s)));
        () ();
      };
    t.Statement : (expr) = <Var-Subst s.tag t.n t.s expr>;
    () ();
  } :: (e.st-pats) (e.st-repls),
    <Var-Subst s.tag t.n t.s e.rest> :: (e.pats) (e.repls),
    (e.st-pats e.pats) (e.st-repls e.repls);
  () ();
};


/////////////////////////// Variables Using Analysis /////////////////////////
//
//$func Post-Comp (e.used-vars) e.comp-func = (e.used-vars) e.result-func;
//
//Post-Comp (e.used-vars) e.comp-func, e.comp-func : {
//  /*
//   * As well as "Used" shouldn't be "Declare" statements added?
//   */
//  e.something (Used e.vars) =
//    <Post-Comp (<Or (e.used-vars) e.vars>) e.something>;
//  e.something (If-used (e.vars) e.statements), {
//    <Split &Elem? e.vars (e.used-vars)> : (v.true-used) (e.yet-not-used) =
//      <Post-Comp (v.true-used) e.statements> :: (e.expr-vars) e.expr,
//      <Post-Comp (<Or (e.yet-not-used) e.expr-vars>) e.something> e.expr;
//    <Post-Comp (e.used-vars) e.something>;
//  };
//  e.something (e.expr) =
//    <Post-Comp (e.used-vars) e.expr> :: (e.expr-vars) e.expr,
//    <Post-Comp (e.expr-vars) e.something> (e.expr);
//  e.something s.symbol =
//    <Post-Comp (e.used-vars) e.something> s.symbol;
//  /*empty*/ = (e.used-vars);
//};


/////////////////////////// Static Clash Analysis ///////////////////////////
//
//$func? Split-Clashes (e.clashes) e.Snt =
//  (e.greater) (e.less) (e.hards) (e.clashes) e.Snt;
//
//$func? Improve-Clash (e.Re) (s.dir e.Pe) (e1) (e2) e.Snt = e.clashes (e.Snt);
//
//$func? Self-Occur (e.Re) e.Pe = e;
//
//$func Cyclic e.expr = e.cyclic-vars;
//
//$func Hard e.expr = e.hard-part;
//
//$func Exchange (e.var-holder) (e.new-expr) e.clashes (e.Snt) =
//  e.clashes (e.Snt);
//
//$func Exchange-Exp (e.change) (e1) (e2) e.Snt = (e1) (e2) e.Snt;
//
//$func Minimize (e.expr) (e.clashes) e.Snt = (e.clashes) (e.less) e.Snt;
//
//$func? Intersect s.k (e.l) s.m (e.n) = s.x (e.y);
//
//$func Min-Length e.expr = s.min-length;
//
//$func Max-Length e.expr = e.max-length;
//
//$func? Add-Less-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt =
//  (e.clashes1) (e.clashes2) e.Snt;
//
//$func? Add-Greater-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt =
//  (e.clashes1) (e.clashes2) e.Snt;
//
//$func Get-Min e.vars = s.min;
//
//$func Get-Max e.vars = e.max;
//
//$func Mults e.vars = e.mults;
//
//$func Mark-Unw-Hard (e.vars) e.clashes = e.clashes;
//
//$func Ceil s1 s2 = s;
//
//$func? Match-Exp (e.Re) e.Pe = s.left s.right;
//
//$func? Match e.clash = ;
//
//$func? Match-Term t.Rt t.Pt e.clashes = e.clashes;
//
//$func? Match-Cyclic (e.Re) (e.Pe) e.clashes = e.clashes;
//
//$func Granulate e.expr = e.expr;
//
//$func? Left-Exp s.left s.len e.expr = (e.expr) e.change;
//
//$func? Right-Exp s.right s.len e.expr = (e.expr) e.change;
//
//$func? Middle-Exp s.left s.right e.expr = (e.expr) e.change;
//
*$func Comp-Pattern t.Pattern e.Snt = e.asail-Snt;
*
*Comp-Pattern (s.dir e.PatternExp) e.Sentence =
*	<Norm-Vars (<Vars e.PatternExp>) (s.dir e.PatternExp) e.Sentence>
*		: t t.Pattern e.Snt,
*//	(Unwatched (<? &Last-Re>) t.Pattern) e.Snt $iter {
*	/*
*	 * Uncomment previous line and delete next one to activate Split-Clashes
*	 * function
*	 */
*	((<? &Last-Re>) t.Pattern) e.Snt $iter {
*		e.Snt : (RESULT e.Re) (s.d e.Pe) e =
*//			<WriteLN Matching (RESULT e.Re) (s.d e.Pe)>,
*			<Norm-Vars (<Vars e.Pe>) e.Snt> : t t.R t.P e.rest,
*//			(e.clashes Unwatched (e.Re) t.P) e.rest;
*			/*
*			 * Uncomment previous line and delete next one to activate
*			 * Split-Clashes function
*			 */
*			(e.clashes (e.Re) t.P) e.rest;
*	} :: (e.clashes) e.Snt,
*	# \{
*		e.Snt : \{
*			(RESULT e.Re) (LEFT e) e = e.Re;
*			(RESULT e.Re) (RIGHT e) e = e.Re;
*		} :: e.Re,
*			<Without-Calls? e.Re>;
*	} =
*	e.Snt : e.Current-Snt (Comp Sentence) e.Other-Snts =
*	<Comp-Sentence () e.Other-Snts> :: e.asail-Others,
*	{
*//		<Split-Clashes (e.clashes) e.Current-Snt>
*//		:: (e.greater) (e.less) (e.hards) (e.clashes) e.Current-Snt =
*//			<WriteLN "Hards: " e.hards>,
*//			<WriteLN "Less: " e.less>,
*//			<WriteLN "Greater: " e.greater>,
*//			<WriteLN "Current-Snt: " e.Current-Snt>,
*//!			<Comp-Clashes (e.clashes)
*//!				(e.Current-Snt (Comp Sentence)) e.Other-Snts> :: e.asail-Clashes,
*//			e.asail-Clashes (e.greater) $iter {
*//				e.greater : (e.vars s.num) e.rest,
*//					<Old-Vars e.vars> :: e.vars,  // temporary step
*//					(IF ((INFIX ">=" ((LENGTH e.vars)) (s.num)))
*//						e.asail-Clashes
*//					) (e.rest);
*//			} :: e.asail-Clashes (e.greater),
*//			e.greater : /*empty*/ =
*//			e.asail-Clashes (e.less) $iter {
*//				e.less : (e.vars s.num) e.rest,
*//					<Old-Vars e.vars> :: e.vars,  // temporary step
*//					(IF ((INFIX "<=" ((LENGTH e.vars)) (s.num)))
*//						e.asail-Clashes
*//					) (e.rest);
*//			} :: e.asail-Clashes (e.less),
*//			e.less : /*empty*/ =
*//			e.asail-Clashes (e.hards) $iter {
*//				e.hards : (e.Re) (e.Pe) e.rest,
*//					<Old-Vars e.Re> :: e.Re,    // temporary step
*//					<Old-Vars e.Pe> :: e.Pe,    // temporary step
*//					(IF ((INFIX "==" (e.Re) (e.Pe))) e.asail-Clashes) (e.rest);
*//			} :: e.asail-Clashes (e.hards),
*//			e.hards : /*empty*/ =
*//!			e.asail-Clashes e.asail-Others;
*		e.asail-Others;
*//		<Comp-Sentence () e.Other-Snts>;
*	};
//
//Split-Clashes (e.clashes) e.Snt =
//  e.clashes (e.Snt) () () () $iter e.clashes : {
//    e1 Unwatched (e.Re) (s.dir e.Pe) e2, { \?
//      \{ 
//        \{
//          <Self-Occur (e.Re) e.Pe> : {
//            Occur e.vars =
//              <Minimize (e.vars) (e1 e2) e.Snt>
//                :: (e.clashes) (e.new-less) e.Snt,
//              e.clashes (e.Snt)
//              (e.greater) (e.less e.new-less) (e.hards);
//            /*empty*/ \! $fail;
//          };
//          <Self-Occur (e.Pe) e.Re> : {
//            Occur e.vars =
//              <Minimize (e.vars) (e1 e2) e.Snt>
//                :: (e.clashes) (e.new-less) e.Snt,
//              e.clashes (e.Snt)
//              (e.greater) (e.less e.new-less) (e.hards);
//            /*empty*/ \! $fail;
//          };
//        };
//        <Vars e.Re> : /*empty*/, \{ // e.Re is ground expression
//          <Vars e.Pe> : /*empty*/ \! // e.Pe is ground expression
//            $fail;
//          e.Pe : \{
//            /*
//             * If e.Pe is symbol then e.Re should be a symbol and if
//             * e.Pe is "old" variable then we should remember clash
//             * "e.Re : e.Pe" as hard.
//             */
//            (SVAR 1 (1) e.name) \!
//              e.Re : s, 
//              {
//                <Known-Vars? (SVAR e.name)> = (e.Re) (e.Pe);
//                /*empty*/;
//              } :: e.new-hard,
//              <Exchange (e.Pe) (e.Re) e1 e2 (e.Snt)>
//                (e.greater) (e.less) (e.hards e.new-hard);
//            /* 
//             * If e.Pe is parenthesized expression then e.Re should be
//             * parenthesized expression too and we can take parentheses
//             * off.
//             */
//            (PAREN e.pat-expr) \!
//              e.Re : (PAREN e.re-expr),
//              e1 Unwatched (e.re-expr) (s.dir e.pat-expr) e2
//              (e.Snt) (e.greater) (e.less) (e.hards);
//            /*
//             * If e.Pe is any other variable then length of e.Re (which
//             * can be zero) should belong to its range. If e.Pe is
//             * "old" variable and e.Re is empty expression then we
//             * should remember that length of e.Pe is less or equal to
//             * 0 and if e.Re isn't empty then we should remember clash
//             * "e.Re : e.Pe" as hard.
//             */
//            (s.var-tag s.m (e.n) e.name) \!
//              <Intersect s.m (e.n) <Length e.Re> (<Length e.Re>)> : e,
//              {
//                <Known-Vars? (s.var-tag e.name)>,
//                  {
//                    e.Re : /*empty*/ = (e.Pe 0) ();
//                    /*empty*/ ((e.Re) (e.Pe));
//                  };
//                /*empty*/ ();
//              } :: e.new-less (e.new-hard),
//              <Exchange (e.Pe) (e.Re) e1 e2 (e.Snt)>
//              (e.greater) (e.less e.new-less) (e.hards e.new-hard);
//          };
//        };
//        <Vars e.Pe> : /*empty*/, e.Re : \{
//          (SVAR 1 (1) e.name) \!
//            e.Pe : s, 
//            {
//              <Known-Vars? (SVAR e.name)> = (e.Re) (e.Pe);
//              /*empty*/;
//            } :: e.new-hard,
//            <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
//              (e.greater) (e.less) (e.hards e.new-hard);
//          (PAREN e.re-expr) \!
//            e.Pe : (PAREN e.pe-expr),
//            e1 Unwatched (e.re-expr) (s.dir e.pe-expr) e2
//            (e.Snt) (e.greater) (e.less) (e.hards);
//          (s.var-tag s.m (e.n) e.name) \!
//            <Intersect s.m (e.n) <Length e.Pe> (<Length e.Pe>)> : e,
//            {
//              <Known-Vars? (s.var-tag e.name)>,
//                {
//                  e.Pe : /*empty*/ = (e.Re 0) ();
//                  /*empty*/ ((e.Re) (e.Pe));
//                };
//              /*empty*/ ();
//            } :: e.new-less (e.new-hard),
//            <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
//            (e.greater) (e.less e.new-less) (e.hards e.new-hard);
//        };
//        e.Re : \{
//          (PAREN e.re-expr), e.Pe : \{
//            (PAREN e.pe-expr) =
//              e1 Unwatched (e.re-expr) (s.dir e.pe-expr) e2
//              (e.Snt) (e.greater) (e.less) (e.hards);
//            (SVAR e) \!
//              $fail;
//            (s.tag s.m (e.n) e.var-id) \!
//              e.var-id : e.NEW (e.QualifiedName),
//              <Intersect 1 (1) s.m (e.n)> :: e,
//              (s.tag 0 () NEW ("paren" e.QualifiedName)) :: t.new-var,
//              {
//                <Known-Vars? (s.tag e.var-id)> =
//                  Watched (e.Pe) (s.dir (PAREN t.new-var));
//                /*empty*/;
//              } :: e.new-clash,
//              <Exchange (e.Pe) ((PAREN t.new-var)) e1 ()> :: e1 t,
//              e.new-clash e1 Unwatched (e.re-expr) (s.dir t.new-var)
//              <Exchange (e.Pe) ((PAREN t.new-var)) e2 (e.Snt)>
//              (e.greater) (e.less) (e.hards);
//          };
//          (SVAR 1 (1) e.name), e.Pe : \{
//            s.ObjectSymbol =
//              {
//                <Known-Vars? (SVAR e.name)> = (e.Re) (e.Pe);
//                /*empty*/;
//              } :: e.new-hard,
//              <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
//              (e.greater) (e.less) (e.hards e.new-hard);
//            (PAREN e) \!
//              $fail;
//            (s.tag s.m (e.n) e.var-id) \!
//              <Intersect 1 (1) s.m (e.n)> :: e,
//              {
//                <Known-Vars? (s.tag e.var-id)>, {
//                  <Known-Vars? (SVAR e.name)> =
//                    ((e.Re) (e.Pe)) ();
//                  () (Watched (e.Pe) (s.dir e.Re));
//                };
//                () ();
//              } :: (e.new-hard) (e.new-clash),
//              e.new-clash <Exchange (e.Pe) (e.Re) e1 e2 (e.Snt)>
//              (e.greater) (e.less) (e.hards e.new-hard);
//          };
//          (s.tag s.m (e.n) e.var-id), TVAR VVAR EVAR : e s.tag e, \{
//            e.Pe : (s.tag1 s.k (e.l) e.var-id1),
//              TVAR VVAR EVAR : e s.tag1 e \!
//              <Intersect s.m (e.n) s.k (e.l)> :: s.x (e.y),
//              {
//                <Known-Vars? (s.tag e.var-id)>, {
//                  <Known-Vars? (s.tag1 e.var-id1)> =
//                    (s.tag s.x (e.y) e.var-id) (e.Re) (e.Pe);
//                  (s.tag s.x (e.y) e.var-id) /*empty*/;
//                };
//                (s.tag1 s.x (e.y) e.var-id1) /*empty*/;
//              } :: t.new-var e.new-hards,
//              <Exchange (e.Re) (t.new-var) e1 e2 (e.Snt)>
//                :: e.clashes (e.Snt),
//              <Exchange (e.Pe) (t.new-var) e.clashes (e.Snt)>
//              (e.greater) (e.less) (e.hards e.new-hards);
//          };
//        };
//        e.Pe : \{
//          (PAREN e.pe-expr), e.Re : \{
//            (s.tag s.m (e.n) e.var-id) \!
//              e.var-id : e.NEW (e.QualifiedName),
//              <Intersect 1 (1) s.m (e.n)> :: e,
//              (s.tag 0 () NEW ("paren" e.QualifiedName)) :: t.new-var,
//              {
//                <Known-Vars? (s.tag e.var-id)> =
//                  Watched (e.Re) (s.dir (PAREN t.new-var));
//                /*empty*/;
//              } :: e.new-clash,
//              <Exchange (e.Re) ((PAREN t.new-var)) e1 ()> :: e1 t,
//              e.new-clash e1 Unwatched (t.new-var) (s.dir e.pe-expr)
//              <Exchange (e.Re) ((PAREN t.new-var)) e2 (e.Snt)>
//              (e.greater) (e.less) (e.hards);
//          };
//          (SVAR 1 (1) e.name), e.Re : \{
//            (s.tag s.m (e.n) e.var-id) \!
//              <Intersect 1 (1) s.m (e.n)> :: e,
//              {
//                <Known-Vars? (s.tag e.var-id)>, {
//                  <Known-Vars? (SVAR e.name)> =
//                    ((e.Re) (e.Pe)) ();
//                  () (Watched (e.Re) (s.dir e.Pe));
//                };
//                () ();
//              } :: (e.new-hard) (e.new-clash),
//              e.new-clash <Exchange (e.Re) (e.Pe) e1 e2 (e.Snt)>
//              (e.greater) (e.less) (e.hards e.new-hard);
//          };
//        };
//        e.Re : t.Rt e.Re1, e.Pe : t.Pt e.Pe1,
//          <Min-Length t.Rt> :: s.rt-min, <Min-Length t.Pt> :: s.pt-min,
//          # \{ s.rt-min : 0; s.pt-min : 0; } =
//          {
//            <Left-Exp 0 s.rt-min t.Pt> (<Left-Exp 0 s.rt-min t.Rt>);
//            <Left-Exp 0 s.pt-min t.Rt> (<Left-Exp 0 s.pt-min t.Pt>);
//          } :: t e.change1 (t e.change2),
//          e1 Unwatched (e.Re) (e.Pe) :: e1,
//          <Exchange-Exp (e.change1)
//            <Exchange-Exp (e.change2) (e1) (e2) e.Snt>>
//            :: (e1) (e2) e.Snt,
//          {
//            e.change1 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
//              <Known-Vars? (s.tag e.var-id)> =
//              Watched
//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
//            /*empty*/;
//          } :: e.new-clash1,
//          {
//            e.change2 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
//              <Known-Vars? (s.tag e.var-id)> =
//              Watched
//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
//            /*empty*/;
//          } :: e.new-clash2,
//          e1 : e11 (t.Rt1 e.Re2) (t.Pt1 e.Pe2),
//          e.new-clash1 e.new-clash2 e11 (t.Rt1) (s.dir t.Pt1)
//          Unwatched (e.Re2) (s.dir e.Pe2) e2
//          (e.Snt) (e.greater) (e.less) (e.hards);
//        e.Re : e.Re1 t.Rt, e.Pe : e.Pe1 t.Pt,
//          <Min-Length t.Rt> :: s.rt-min, <Min-Length t.Pt> :: s.pt-min,
//          # \{ s.rt-min : 0; s.pt-min : 0; } =
//          {
//            <Right-Exp 0 s.rt-min t.Pt> (<Right-Exp 0 s.rt-min t.Rt>);
//            <Right-Exp 0 s.pt-min t.Rt> (<Right-Exp 0 s.pt-min t.Pt>);
//          } :: t e.change1 (t e.change2),
//          e1 Unwatched (e.Re) (e.Pe) :: e1,
//          <Exchange-Exp (e.change1)
//            <Exchange-Exp (e.change2) (e1) (e2) e.Snt>>
//            :: (e1) (e2) e.Snt,
//          {
//            e.change1 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
//              <Known-Vars? (s.tag e.var-id)> =
//              Watched
//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
//            /*empty*/;
//          } :: e.new-clash1,
//          {
//            e.change2 : (s.tag t.m t.n e.var-id) t.new-1 t.new-2,
//              <Known-Vars? (s.tag e.var-id)> =
//              Watched
//              ((s.tag t.m t.n e.var-id)) (s.dir t.new-1 t.new-2);
//            /*empty*/;
//          } :: e.new-clash2,
//          e1 : e11 (e.Re2 t.Rt1) (e.Pe2 t.Pt1),
//          e.new-clash1 e.new-clash2 e11 (e.Re2) (s.dir e.Pe2)
//          Unwatched (t.Rt1) (s.dir t.Pt1) e2
//          (e.Snt) (e.greater) (e.less) (e.hards);
//        <Max-Length e.Re> : /*empty*/, <Max-Length e.Pe> : /*empty*/ \!
//          <Min-Length e.Re> :: s.re-min,
//          <Min-Length e.Pe> :: s.pe-min,
//          e1 Unwatched Hard (e.Re) (s.dir e.Pe) :: e1,
//          {
//            <"<" (s.re-min) (s.pe-min)> =
//              <Add-Greater-Ineq (<Cyclic e.Re> s.pe-min)
//                (e1) (e2) e.Snt>;
//            <">" (s.re-min) (s.pe-min)> =
//              <Add-Greater-Ineq (<Cyclic e.Pe> s.re-min)
//                (e1) (e2) e.Snt>;
//            (e1) (e2) e.Snt;
//          } :: (e1) (e2) e.Snt,
//          e1 e2 (e.Snt) (e.greater) (e.less) (e.hards);
//        {
//          <Max-Length e.Re> : s.re-max, {
//            <Max-Length e.Pe> : s.pe-max, {
//              <"<" (s.re-max) (s.pe-max)> = e.Pe s.re-max;
//              e.Re s.pe-max;
//            };
//            e.Pe s.re-max;
//          };
//          e.Re <Max-Length e.Pe>;
//        } : e.ineq s.max \!
//          <"-" s.max <Min-Length <Hard e.ineq>>> :: s.max,
//          <Cyclic e.ineq> :: e.cyclic,
//          <Add-Less-Ineq (e.cyclic s.max)
//            (e1 Unwatched Hard (e.Re) (s.dir e.Pe)) (e2) e.Snt>
//            :: (e1) (e2) e.Snt \?
//          {
//            e1 : e Unwatched Hard t t \!
//              <Min-Length e.Re> :: s.re-min,
//              <Min-Length e.Pe> :: s.pe-min,
//              {
//                <"<" (s.re-min) (s.pe-min)> = e.Re s.pe-min;
//                e.Pe s.re-min;
//              } :: e.ineq s.min,
//              <"-" s.min <Min-Length <Hard e.ineq>>> :: s.min,
//              <Cyclic e.ineq> :: e.cyclic,
//              <Add-Greater-Ineq (e.cyclic s.min) (e1) (e2) e.Snt>
//                :: (e1) (e2) e.Snt,
//              e1 e2 (e.Snt) (e.greater) (e.less) (e.hards);
//            e1 e2 (e.Snt) (e.greater) (e.less) (e.hards);
//          };
//      };
//      = <Print-Error Warning! Pattern (e.Re ' : ' e.Pe)>, $fail;
//    };
//    e1 Unwatched Hard (e.Re) (s.dir e.Pe) e2, {
//      <Cyclic e.Re> : /*empty*/, {  // e.Re is hard expression
//        <Improve-Clash (e.Re) (s.dir e.Pe) (e1) (e2) e.Snt>
//          (e.greater) (e.less) (e.hards);
//        <Print-Error Warning! Pattern (e.Re ' : ' e.Pe)>
//          = $fail;
//      };
////      <Cyclic e.Pe> : /*empty*/ = // e.Pe is hard expression
////        <Improve-Clash (e.Pe) (e.Re) (e1) (e2) e.Snt>
////        (e.greater) (e.less) (e.hards);
//      e1 (e.Re) (s.dir e.Pe) e2 (e.Snt) (e.greater) (e.less) (e.hards);
//    };
//    e1 Watched t.Re t.Pe e2 =
//      e1 t.Re t.Pe e2 (e.Snt) (e.greater) (e.less) (e.hards);
//  } :: e.clashes (e.Snt) (e.greater) (e.less) (e.hards),
////  <WriteLN Sp-Clashes e.clashes>,
////  <WriteLN G <? &Greater-Ineqs>>,
////  <WriteLN L <? &Less-Ineqs>>,
//  # \{ e.clashes : e s e; } =
//  (e.greater) (e.less) (e.hards) (e.clashes) e.Snt;
//
//Improve-Clash (e.Re) (s.dir e.Pe) (e1) (e2) e.Snt =
////  <WriteLN Improve-Clash (e.Re) (s.dir e.Pe)>,
//  /*
//   * Find all non-empty hard parts in e.Pe and remember them in
//   * e.hard-parts.
//   */
//  e.Pe : t.l e.right,
//  () (t.l) (e.right) <Cyclic e.right> $iter {
//    e.cyclic : t.var e.rest,
//      e.right : e.new-hard t.var e.new-right, {
//        e.new-hard : v =
//          (e.hard-parts 
//            ((e.left) e.new-hard (t.var e.new-right))
//          ) (e.left e.new-hard t.var) (e.new-right) e.rest;
//        (e.hard-parts) (e.left t.var) (e.new-right) e.rest;
//      };
//  } :: (e.hard-parts) (e.left) (e.right) e.cyclic,
//  e.cyclic : /*empty*/ =
////  <WriteLN Hard-parts e.hard-parts>,
//  /*
//   * For each hard part (or until some variables ranges are
//   * changed or some inequalitys are added) try to match it with
//   * corresponding part of e.Re.
//   */
//  (e.hard-parts)
//  (e1 (e.Re) (s.dir e.Pe)) (e2) e.Snt $iter {
//    e.hard-parts : ((e.left-i) e.hard-i (e.right-i)) e.rest,
//      <Cyclic e.left-i> :: e.cyc-left,
//      <Hard e.left-i> :: e.hard-left,
//      <Reverse <Cyclic e.right-i>> :: e.cyc-right,
//      <Hard e.right-i> :: e.hard-right,
//      <Min-Length e.hard-left> :: s.left-len,
//      <Min-Length e.hard-right> :: s.right-len,
//      <"+" <Get-Min e.cyc-left> s.left-len> :: s.left-min,
//      <Get-Max e.cyc-left> : s.left-max,
//      <"+" s.left-max s.left-len> :: s.left-max,
//      <"+" <Get-Min e.cyc-right> s.right-len> :: s.right-min,
//      <Get-Max e.cyc-right> : s.right-max,
//      <"+" s.right-max s.right-len> :: s.right-max,
//      <Min-Length e.hard-i> :: s.hard-len,
//      <Min-Length e.Re> :: s.len,
//      <"-" s.len <"+" s.right-max s.hard-len>> :: s.left,
//      <"-" s.len <"+" s.left-max s.hard-len>> :: s.right,
//      <WriteLN Hard e.hard-i>,
//      <WriteLN Hard-len s.hard-len>,
//      <WriteLN Left-len s.left-len>,
//      <WriteLN Right-len s.right-len>,
//      <WriteLN Len s.len>,
//      <WriteLN Left s.left>,
//      <WriteLN Left-min s.left-min>,
//      <WriteLN Left-max s.left-max>,
//      <WriteLN Right s.right>,
//      <WriteLN Right-min s.right-min>,
//      <WriteLN Right-max s.right-max>,
//      {
//        s.left-min : s.left, s.right-min : s.right =
//          <Middle-Exp s.left s.right e.Re> :: (e.middle) e.change,
//          <WriteLN Middle-Exp e.middle>,
//          <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
//          <Match-Exp (e.middle) e.hard-i> :: s.new-left s.new-right,
//          <WriteLN Match-Exp s.new-left s.new-right>,
//          {
//            s.new-left : 0, s.new-right : 0 =
//              (e.rest) (e1) (e2) e.Snt;
//            /*
//             * If founded matchings are coinsided then split our
//             * clash into three new ones.
//             */
//            <"+" s.hard-len <"+" s.new-left s.new-right>>
//            : s.len =
//              <"+" s.left s.new-left> :: s.left,
//              <"+" s.right s.new-right> :: s.right,
//              <Left-Exp s.left s.hard-len e.Re> :: (e.left-Re) e.change,
//              <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
//              Unwatched (e.left-Re) (s.dir e.hard-i) :: e.new-hard,
//              <Left-Exp 0 s.left e.Re> :: (e.left-Re) e.change,
//              <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
//              Unwatched (e.left-Re) (s.dir e.left-i) :: e.new-left,
//              <Right-Exp 0 s.right e.Re> :: (e.right-Re) e.change,
//              <Exchange-Exp (e.change) (e1) (e2) e.Snt> :: (e1) (e2) e.Snt,
//              Unwatched (e.right-Re) (s.dir e.right-i) :: e.new-right,
//              s.dir : {
//                LEFT = 
//                  e.new-hard e.new-left e.new-right;
//                RIGHT =
//                  e.new-hard e.new-right e.new-left;
//              } :: e.new-clashes,
//              e1 : e1-new t t,
//              () (e1-new e.new-clashes) (e2) e.Snt;
//            /*
//             * Else we've got some new inequalites...
//             */
//            =
//              <"+" s.left <"-" s.new-left s.left-len>> :: s.num,
//              <WriteLN NUM s.num>,
//              <Add-Greater-Ineq (e.cyc-left s.num) (e1) (e2) e.Snt>
//                :: (e1) (e2) e.Snt,
//              <"+" s.right <"-" s.new-right s.right-len>> :: s.num,
//              <WriteLN NUM s.num>,
//              <Add-Greater-Ineq (e.cyc-right s.num) (e1) (e2) e.Snt>
//                :: (e1) (e2) e.Snt,
//              <"-" s.len <"+" s.right <"+" s.new-right
//                <"+" s.hard-len s.left-len>>>> :: s.num,
//              <WriteLN NUM s.num>,
//              <Add-Less-Ineq (e.cyc-left s.num) (e1) (e2) e.Snt>
//                :: (e1) (e2) e.Snt,
//              <"-" s.len <"+" s.left <"+" s.new-left
//                <"+" s.hard-len s.right-len>>>> :: s.num,
//              <WriteLN NUM s.num>,
//              <Add-Less-Ineq (e.cyc-right s.num) (e1) (e2) e.Snt>
//                :: (e1) (e2) e.Snt,
//              (e.rest) (e1) (e2) e.Snt;
//          };
//        /*
//         * At least one inequlity shurely will be added, so we'll go
//         * out of the $iter.
//         */
//        = {
//          <"<" (s.left-min) (s.left)> =
//            <Add-Greater-Ineq (e.cyc-left s.left) (e1) (e2) e.Snt>;
//          (e1) (e2) e.Snt;
//        } :: (e1) (e2) e.Snt, {
//          <">" (s.left-min) (s.left)> =
//            <"-" s.len <"+" s.left-min <"+" s.hard-len s.right-len>>>
//              :: s.left,
//            <Add-Less-Ineq (e.cyc-right s.left) (e1) (e2) e.Snt>;
//          (e1) (e2) e.Snt;
//        } :: (e1) (e2) e.Snt, {
//          <"<" (s.right-min) (s.right)> =
//            <Add-Greater-Ineq (e.cyc-right s.right) (e1) (e2) e.Snt>;
//          (e1) (e2) e.Snt;
//        } :: (e1) (e2) e.Snt, {
//          <">" (s.right-min) (s.right)> =
//            <"-" s.len <"+" s.right-min <"+" s.hard-len s.left-len>>>
//              :: s.right,
//            <Add-Less-Ineq (e.cyc-left s.right) (e1) (e2) e.Snt>;
//          (e1) (e2) e.Snt;
//        } :: (e1) (e2) e.Snt,
//          () (e1) (e2) e.Snt;
//      };
//  } :: (e.hard-parts) (e1) (e2) e.Snt,
//  \{
//    e1 : \{ e Unwatched (e) (e); e Unwatched Hard (e) (e); };
//    e.hard-parts : /*empty*/;
//  } =
//  e1 e2 (e.Snt);
//
///*
// * If occurrence of e.Pe is found in e.Re and it can be there then return
// * variables which should be minimized.
// * If found occurence of e.Re isn't legal then return empty expression.
// * And return $fail if there are no occurences of e.Re in e.Pe.
// */
//Self-Occur (e.Re) e.Pe, <WriteLN Occur (e.Re) e.Pe>, {
//  e.Re : e1 e.Pe e2 , {
//    <Min-Length e1 e2> : 0 = Occur e1 e2;
//    /*empty*/;
//  };
//  e.Pe Not-Found $iter {
//    e.Pe : e (PAREN v.pe-expr) e, {
//      e.Re : e v.pe-expr e = Found;
//      v.pe-expr Not-Found;
//    };
//  } :: e.Pe s.found?,
//  \{
//    s.found? : Found = /*empty*/;
//    # \{ e.Pe : e (PAREN v) e; } = $fail;
//  };
//};
//
//Cyclic e.expr = 
//  () e.expr $iter {
//    e.expr : t1 e2, t1 : {
//      s.ObjectSymbol = /*empty*/;
////      (REF t.name) = ???
//      (PAREN e) = /*empty*/;
//      (s.var-tag s.m (e.n) e.var-id), # \{ s.m : e.n; } = t1;
//      t = /*empty*/;
//    } :: e.new-cyclic,
//    (e.cyclic e.new-cyclic) e2;
//  } :: (e.cyclic) e.expr,
//  e.expr : /*empty*/ =
//  e.cyclic;
//
//Hard e.expr = 
//  () e.expr $iter {
//    e.expr : t1 e2, t1 : {
//      s.ObjectSymbol = t1;
////      (REF t.name) = ???
//      (PAREN e) = t1;
//      (s.var-tag s.m (e.n) e.var-id), # \{ s.m : e.n; } = /*empty*/;
//      t = t1;
//    } :: e.new-hard,
//    (e.hard e.new-hard) e2;
//  } :: (e.hard) e.expr,
//  e.expr : /*empty*/ =
//  e.hard;
//
////Hard-Exp? e.expr =
////  e.expr () $iter \{
////    <Cyclic e.expr> () $iter {
////      e.cyclic : (s.tag t t e.var-id) e.rest, {
////        <Known-Vars? (s.tag e.var-id)> = e.rest (e.num);
////        e.rest (e.num I);
////      };
////    } :: e.cyclic (e.num),
////      <WriteLN Hard-Exp e.cyclic (e.num)>,
////      \{
////        e.num : I I = $fail;
////        e.cyclic : /*empty*/, {
////          e.expr : e1 (PAREN e.paren) e2 = e.paren (e.watched e2);
////          e.watched : e1 (PAREN e.paren) e2 = e.paren (e2);
////          /*empty*/ ();
////        };
////      };
////  } :: e.expr (e.watched),
////  e.expr : /*empty*/;
//
//Exchange (e.var-holder) (e.new-expr) e.clashes (e.Snt) =
//  e.var-holder : t.var,
//  /*
//   * Mark containing t.var clashes as "Unwatched" and change t.var to
//   * t.new-var in them.
//   */
//  () e.clashes $iter {
//    e.clashes : e.tag (e.Re) (e.Pe) e.rest,
//      {
//        e.tag : Watched = Watched;
//        Unwatched;
//      } :: s.watched?,
//      {
//        <Vars e.Re> <Vars e.Pe> : e t.var e =
//          (e.new-clashes
//          s.watched? <Subst (t.var) ((e.new-expr)) (e.Re) (e.Pe)>
//          ) e.rest;
//        (e.new-clashes e.tag (e.Re) (e.Pe)) e.rest;
//      };
//  } :: (e.new-clashes) e.clashes,
//  e.clashes : /*empty*/ =
//  /*
//   * Remove all inequalitys wich contain t.var.
//   */
//  () <? &Greater-Ineqs> $iter {
//    e.ineqs : t.ineq e.rest, 
//      {
//        t.ineq : (e t.var e) = /*empty*/;
//        t.ineq;
//      } :: e.ineq,
//      (e.new-ineqs e.ineq) e.rest;
//  } :: (e.new-ineqs) e.ineqs,
//  e.ineqs : /*empty*/ =
//  <Store &Greater-Ineqs e.new-ineqs>,
//  () <? &Less-Ineqs> $iter {
//    e.ineqs : t.ineq e.rest, 
//      {
//        t.ineq : (e t.var e) = /*empty*/;
//        t.ineq;
//      } :: e.ineq,
//      (e.new-ineqs e.ineq) e.rest;
//  } :: (e.new-ineqs) e.ineqs,
//  e.ineqs : /*empty*/ =
//  <Store &Less-Ineqs e.new-ineqs>,
//  /*
//   * Rename t.var in the rest of current sentence.
//   */
//  t.var : (s.tag t t e.var-id),     // temporary step
////  <Old-Vars e.new-expr> :: e.new-expr,  // temporary step
//  e.new-clashes (<Subst ((s.tag e.var-id)) ((e.new-expr)) e.Snt>);
//
//Exchange-Exp (e.change) (e1) (e2) e.Snt =
//{
//  e.change : t.old-1 t.new-1 t.new-2 e.change1 =
//    <Exchange (t.old-1) (t.new-1 t.new-2) e1 ()> :: e1 t,
//    <Exchange (t.old-1) (t.new-1 t.new-2) e2 (e.Snt)> :: e2 (e.Snt),
//    {
//      e.change1 : t.old-2 e.new-3 =
//        <Exchange (t.old-2) (e.new-3) e1 ()> :: e1 t,
//        <Exchange (t.old-2) (e.new-3) e2 (e.Snt)> :: e2 (e.Snt),
//        (e1) (e2) e.Snt;
//      (e1) (e2) e.Snt;
//    };
//  (e1) (e2) e.Snt;
//};
//
//Minimize (e.expr) (e.clashes) e.Snt =
//  (e.expr) () e.clashes (e.Snt) $iter {
//    e.expr : t.var e.rest,
//      t.var : (s.tag t t e.var-id),
//      {
//        <Known-Vars? (s.tag e.var-id)> = (t.var 0);
//        /*empty*/;
//      } :: e.new-less,
//      (e.rest) (e.less e.new-less) <Exchange (t.var) () e.clashes (e.Snt)>;
//  } :: (e.expr) (e.less) e.clashes (e.Snt),
//  e.expr : /*empty*/ =
//  (e.clashes) (e.less) e.Snt;
//
//Intersect s.k (e.l) s.m (e.n) =
//  {
//    <"<" (s.k) (s.m)> = s.m;
//    s.k;
//  } :: s.x,
//  {
//    e.l e.n : /*empty*/ = /*empty*/;
//    e.l : /*empty*/ = e.n;
//    e.n : /*empty*/ = e.l;
//    <"<" (e.n) (e.l)> = e.n;
//    e.l;
//  } :: e.y,
//  \{
//    e.y : /*empty*/ = s.x ();
//    <"<=" (s.x) (e.y)> = s.x (e.y);
//  };
//
//Min-Length e.expr =
//  0 e.expr $iter {
//    e.expr : t1 e2, t1 : {
//      s.ObjectSymbol = <"+" s.len 1>;
////      (REF t.name) = ???
//      (PAREN e) = <"+" s.len 1>;
//      (s.var-tag s.m (e.n) e.var-id) = <"+" s.len s.m>;
//    } :: s.len,
//    s.len e2;
//  } :: s.len e.expr,
//  e.expr : /*empty*/ =
//  s.len;
//
//Max-Length e.expr =
//  0 e.expr $iter {
//    e.expr : t1 e2, t1 : {
//      s.ObjectSymbol = <"+" s.len 1>;
////      (REF t.name) = ???
//      (PAREN e) = <"+" s.len 1>;
//      (s.var-tag s.m (s.n) e.var-id) = <"+" s.len s.n>;
//      (s.var-tag s.m () e.var-id) = Empty;
//    } :: s.len,
//    s.len e2;
//  } :: s.len e.expr,
//  \{
//    s.len : Empty = /*empty*/;
//    e.expr : /*empty*/ = s.len;
//  };
//
//Add-Less-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt =
//  <Get-Min e.vars> :: s.min, {
//    <">" (s.min) (s.len)> = $fail;
//    <Mults e.vars> :: e.mults,
//      <Min-Length e.vars> :: s.min-len,
//      /*
//       * For each variable form new inequality recompute its maximum:
//       *  new_max = (s.len - s.min-len + s.mult * min) / s.mult
//       */
//      () e.vars $iter {
//        e.tmp-vars : (s.tag s.m (e.n) e.var-id) e.rest,
//          e.mults : e (s.tag s.m (e.n) e.var-id) s.mult e,
//          <Div <"+" <"-" s.len s.min-len> <"*" s.mult s.m>> s.mult>
//            :: s.max,
//          {
//            e.n : /*empty*/ = s.max;
//            <"<" (e.n) (s.max)> = e.n;
//            s.max;
//          } :: e.max,
//          (e.new-vars (s.tag s.m (e.max) e.var-id)) e.rest;
//      } :: (e.new-vars) e.tmp-vars,
//      e.tmp-vars : /*empty*/ =
//      <Max-Length e.new-vars> : s.max-len, {
//        /*
//         * Check that maximums weren't decreased too much.
//         */
//        <">" (s.min) (s.max-len)> = $fail;
//        /*
//         * If max-len == <<minimal valid value>> then change all
//         * e*[min,max] to e*[max,max]. If max == 0 then change variable
//         * to empty expression.
//         */
//        s.min : s.max-len =
//          e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
//            e.vars : t.var e.rest,
//              e.new-vars : (s.tag s.m (s.n) e.var-id) e.new-rest, {
//                s.n : 0 =
////                  <Exchange (t.var) () e.clashes1 ()>
////                    :: e.clashes1 t,
////                  <Exchange (t.var) () e.clashes2 (e.Snt)>
////                    :: e.clashes2 (e.Snt),
//                  e.rest (e.new-rest)
//                  (e.clashes1 Unwatched (t.var) (LEFT))
//                  (e.clashes2) (e.Snt);
//                <Exchange (t.var) ((s.tag s.n (s.n) e.var-id))
//                  e.clashes1 ()> :: e.clashes1 t,
//                  <Exchange (t.var) ((s.tag s.n (s.n) e.var-id))
//                    e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
//                  e.rest (e.new-rest) (e.clashes1)
//                    (e.clashes2) (e.Snt);
//              };
//          } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
//          e.vars : /*empty*/ =
//          (e.clashes1) (e.clashes2) e.Snt;
//        /*
//         * If no maximums were changed then see whether we should add
//         * new inequality to storage and if so then mark clashes
//         * containing e.vars in the begining or reversed e.vars in the
//         * end as "Unwatched Hard".
//         */
//        e.vars : e.new-vars, {
//          <">" (<Get-Max e.vars>) (s.len)>,
//            () <? &Less-Ineqs> $iter e.tmp-ineqs : {
//              e1 (e.vars e.ineq s.in-len) e2,
//                <Max-Length e.ineq> : s.ineq-max,
//                <"<=" (<"+" s.len s.ineq-max>) (s.in-len)>,
//                (e.ineqs e1) e2;
//              e1 = (e.ineqs e1);
//            } :: (e.ineqs) e.tmp-ineqs,
//            e.tmp-ineqs : /*empty*/ =
//            {
//              e.ineqs : e1 (e.vars e.ineq) e2 =
//                e1 (e.vars s.len) (e.vars e.ineq) e2;
//              e.ineqs (e.vars s.len);
//            } :: e.ineqs,
//            <Store &Less-Ineqs e.ineqs>,
//            (<Mark-Unw-Hard (e.vars) e.clashes1>)
//            (<Mark-Unw-Hard (e.vars) e.clashes2>)
//            e.Snt;
//          (e.clashes1) (e.clashes2) e.Snt;
//        };
//        /*
//         * Else, if some maximums were changed, then change them in all
//         * clashes and in Snt. For each variable maximum can't be less
//         * then minimum because it would mean that s.len < s.min.
//         * If max == 0 then change variable to empty expression.
//         */
//        e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
//          e.vars : t.var e.rest,
//            e.new-vars : (s.tag s.m (s.n) e.var-id) e.new-rest, {
//              t.var : (s.tag s.m (s.n) e.var-id) =
//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
//              s.n : 0 =
////                <Exchange (t.var) () e.clashes1 ()>
////                  :: e.clashes1 t,
////                <Exchange (t.var) () e.clashes2 (e.Snt)>
////                  :: e.clashes2 (e.Snt),
//                e.rest (e.new-rest)
//                (e.clashes1 Unwatched (t.var) (LEFT)) (e.clashes2)
//                (e.Snt);
//              <Exchange (t.var) ((s.tag s.m (s.n) e.var-id))
//                e.clashes1 ()> :: e.clashes1 t,
//                <Exchange (t.var) ((s.tag s.m (s.n) e.var-id))
//                  e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
//            };
//        } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
//        e.vars : /*empty*/ =
//        (e.clashes1) (e.clashes2) e.Snt;
//      };
//  };
//
//Add-Greater-Ineq (e.vars s.len) (e.clashes1) (e.clashes2) e.Snt, {
//  <Get-Max e.vars> : s.max, {
//    <"<" (s.max) (s.len)> = $fail;
//    <Mults e.vars> :: e.mults,
//      <Max-Length e.vars> : s.max-len,
//      /*
//       * For each variable from new inequality recompute its minimum:
//       *  new_min = ceil ((s.len - s.max-len + s.mult * max) / s.mult)
//       */
//      () e.vars $iter {
//        e.tmp-vars : (s.tag s.m (s.n) e.var-id) e.rest,
//          e.mults : e (s.tag s.m (s.n) e.var-id) s.mult e,
//          <Ceil <"+" <"-" s.len s.max-len> <"*" s.mult s.n>> s.mult>
//            :: s.min,
//          { 
//            <"<" (s.min) (0)> = 0;
//            <">" (s.m) (s.min)> = s.m;
//            s.min;
//          } :: s.min,
//          (e.new-vars (s.tag s.min (s.n) e.var-id)) e.rest;
//      } :: (e.new-vars) e.tmp-vars,
//      e.tmp-vars : /*empty*/ =
//      <Min-Length e.new-vars> :: s.min-len, {
//        /*
//         * Check that minimums weren't increased too much.
//         */
//        <"<" (s.max) (s.min-len)> = $fail;
//        /*
//         * If min-len == <<maximum valid value>> then change all
//         * e*[min,max] to e*[min,min].
//         */
//        s.max : s.min-len =
//          e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
//            e.vars : t.var e.rest,
//              e.new-vars : (s.tag s.m (s.n) e.var-id) e.new-rest,
//              <Exchange (t.var) ((s.tag s.m (s.m) e.var-id))
//                e.clashes1 ()> :: e.clashes1 t,
//              <Exchange (t.var) ((s.tag s.m (s.m) e.var-id))
//                e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
//              e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
//          } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
//          e.vars : /*empty*/ =
//          (e.clashes1) (e.clashes2) e.Snt;
//        /*
//         * If no minimums were changed then see whether we should add
//         * new inequality to storage and if so then mark clashes
//         * containing e.vars in the begining or reversed e.vars in the
//         * end as "Unwatched Hard".
//         */
//        e.vars : e.new-vars, {
//          <"<" (<Get-Min e.vars>) (s.len)>,
//            () <? &Greater-Ineqs> $iter e.tmp-ineqs : {
//              e1 (e.vars e.ineq s.in-len) e2,
//                <">=" (<"+" s.len <Min-Length e.ineq>>) (s.in-len)>,
//                (e.ineqs e1) e2;
//              e1 = (e.ineqs e1);
//            } :: (e.ineqs) e.tmp-ineqs,
//            e.tmp-ineqs : /*empty*/ =
//            {
//              e.ineqs : e1 (e.vars e.ineq) e2 =
//                e1 (e.vars s.len) (e.vars e.ineq) e2;
//              e.ineqs (e.vars s.len);
//            } :: e.ineqs,
//            <Store &Greater-Ineqs e.ineqs>,
//            (<Mark-Unw-Hard (e.vars) e.clashes1>)
//            (<Mark-Unw-Hard (e.vars) e.clashes2>)
//            e.Snt;
//          (e.clashes1) (e.clashes2) e.Snt;
//        };
//        /*
//         * Else, if some minimums were changed, then change them in all
//         * clashes and in Snt. For each variable minimum can't be greater
//         * then maximum because it would mean that s.len > s.max.
//         */
//        e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt) $iter {
//          e.vars : t.var e.rest,
//            e.new-vars : t.new-var e.new-rest, {
//              t.var : t.new-var =
//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
//              <Exchange (t.var) (t.new-var) e.clashes1 ()> 
//                :: e.clashes1 t,
//                <Exchange (t.var) (t.new-var) e.clashes2 (e.Snt)>
//                  :: e.clashes2 (e.Snt),
//                e.rest (e.new-rest) (e.clashes1) (e.clashes2) (e.Snt);
//            };
//        } :: e.vars (e.new-vars) (e.clashes1) (e.clashes2) (e.Snt),
//        e.vars : /*empty*/ =
//        (e.clashes1) (e.clashes2) e.Snt;
//      };
//  };
//  e.vars : (s.tag s.n () e.var-id), {
//    <">" (s.len) (s.n)> =
//      <Exchange ((s.tag s.n () e.var-id)) ((s.tag s.len () e.var-id))
//        e.clashes1 ()> :: e.clashes1 t,
//      <Exchange ((s.tag s.n () e.var-id)) ((s.tag s.len () e.var-id))
//        e.clashes2 (e.Snt)> :: e.clashes2 (e.Snt),
//      (e.clashes1) (e.clashes2) e.Snt;
//    (e.clashes1) (e.clashes2) e.Snt;
//  };
//  (e.clashes1) (e.clashes2) e.Snt;  // STUB!!! Add inequality to the storage?
//};
//
//Get-Min e.vars, {
//  <? &Greater-Ineqs> : $r e (e.ineq s.len) e,
//    e.vars : e.ineq e.other,
//    <"+" s.len <Min-Length e.other>>;
//  <Min-Length e.vars>;
//};
//
//Get-Max e.vars, {
//  <? &Less-Ineqs> : $r e (e.ineq s.len) e,
//    e.vars : e.ineq e.other,
//    <Max-Length e.other> : s.other-len,
//    <"+" s.len s.other-len>;
//  <Max-Length e.vars>;
//};
//
///*
// * Computes variables multiplicitys and returns them in the form:
// *  e.mults ::= t.var s.mult e.mults | []
// */
//Mults e.vars =
//  () e.vars $iter {
//    e.vars : t.var e.rest,
//      1 e.rest $iter {
//        e.rest : e1 t.var e2,
//          <"+" s.mult 1> e1 e2;
//      } :: s.mult e.rest,
//      # \{ e.rest : e t.var e; } =
//      (e.mults t.var s.mult) e.rest;
//  } :: (e.mults) e.vars,
//  e.vars : /*empty*/ =
//  e.mults;
//
//Mark-Unw-Hard (e.vars) e.clashes =
//  <Reverse e.vars> :: e.rev-vars,
//  () e.clashes $iter e.clashes : {
//    (e.Re) (e.Pe) e.rest,
//      <Cyclic e.Re> :: e.cyc-Re,
//      <Cyclic e.Pe> :: e.cyc-Pe,
//      {
//        \{
//          e.cyc-Re : e.vars e;
//          e.cyc-Re : e e.rev-vars;
//          e.cyc-Pe : e.vars e;
//          e.cyc-Pe : e e.rev-vars;
//        },
//          (e.new-clashes Unwatched Hard (e.Re) (e.Pe)) e.rest;
//        (e.new-clashes (e.Re) (e.Pe)) e.rest;
//      };
//    e.tag (e.Re) (e.Pe) e.rest =
//      (e.new-clashes e.tag (e.Re) (e.Pe)) e.rest;
//  } :: (e.new-clashes) e.clashes,
//  e.clashes : /*empty*/ =
//  e.new-clashes;
//
//Ceil s1 s2, {
//  <Rem s1 s2> : 0 = <Div s1 s2>;
//  <"+" <Div s1 s2> 1>;
//};
//
//Match-Exp (e.Re) e.Pe =
//  <Granulate e.Re> :: e.Re,
//  <Granulate e.Pe> :: e.Pe,
//  <Length e.Pe> :: s.len,
//  e.Re : e1 e2,
//  <Match (<Left 0 s.len e2>) (e.Pe)>,
//  e2 : $r e3 e4,
//  <Match (<Right 0 s.len e3>) (e.Pe)>,
//  <Length e1> <Length e4>;
//
//Match e.clash =
//  e.clash $iter e.clashes : \{
//    e1 (e.expr) (e.expr) e2 = e1 e2;
//    e1 (t.Rt e.Re) (t.Pt e.Pe) e2,
//      # \{ t.Rt : (EVAR e); t.Pt : (EVAR e); } =
//      <Match-Term t.Rt t.Pt e1 (e.Re) (e.Pe) e2>;
//    e1 (e.Re t.Rt) (e.Pe t.Pt) e2,
//      # \{ t.Rt : (EVAR e); t.Pt : (EVAR e); } =
//      <Match-Term t.Rt t.Pt e1 (e.Re) (e.Pe) e2>;
//    e1 (e.Re) (e.Pe) e2, \{
//      e.Re : (EVAR e) e (EVAR e) = <Match-Cyclic (e.Re) (e.Pe) e1 e2>;
//      e.Pe : (EVAR e) e (EVAR e) = <Match-Cyclic (e.Pe) (e.Re) e1 e2>;
//      \{
//        e.Re : (EVAR e) e, e.Pe : e (EVAR e);
//        e.Re : (EVAR e) e, e.Pe : e (EVAR e);
//      } =
//        <Intersect <Min-Length e.Re> (<Max-Length e.Re>)
//          <Min-Length e.Pe> (<Max-Length e.Pe>)>; // This is STUB!!!
//    };
//  } :: e.clashes,
//  <WriteLN Match e.clashes>,
//  e.clashes : /*empty*/;
//
//Match-Term {
//  term term e.clashes = e.clashes;
//  t.Rt t.Pt e.clashes, t.Rt : {
//    s.ObjectSymbol =
//      t.Pt : (s.tag e),
//      SVAR TVAR : e s.tag e,  // check that s.tag isn't PAREN
//      <Subst (t.Pt) ((t.Rt)) e.clashes>;
//    (SVAR e), t.Pt : {
//      s.ObjectSymbol = <Subst (t.Rt) ((t.Pt)) e.clashes>;
//      (s.tag e) =
//        SVAR TVAR : e s.tag e,  // check that s.tag isn't PAREN
//        <Subst (t.Pt) ((t.Rt)) e.clashes>;
//    };
//    (TVAR e) =
//      <Subst (t.Rt) ((t.Pt)) e.clashes>;
//    (PAREN e.Re) = t.Pt : \{
//      (TVAR e) = <Subst (t.Pt) ((t.Rt)) e.clashes>;
//      (PAREN e.Pe) = (e.Re) (e.Pe) e.clashes;
//    };
//  };
//};
//
//Match-Cyclic (e.Re) (e.Pe) e.clashes = ;  // This is STUB!!!
//
//Granulate e.expr =
//  (e.expr) <Vars e.expr> $iter {
//    e.vars : t.var e.rest,
//      t.var : {
//        (s.tag 1 (1) e.var-id), {
//          SVAR TVAR : e s.tag e = e.expr;
//          <Subst (t.var) (((TVAR 1 (1)) e.var-id)) e.expr>;
//        };
//        (s.tag s.n (s.n) e.NEW (e.QualifiedName)) =
//          s.n /*empty*/ $iter
//            <"-" s.n 1>
//            (TVAR 1 (1) NEW ("gran" e.QualifiedName s.n)) e.new-vars
//          :: s.n e.new-vars,
//          s.n : 0 =
//          <Subst (t.var) ((e.new-vars)) e.expr>;
//        (s.tag e.something), {  // cyclic variable
//          s.tag : EVAR = e.expr;
//          <Subst (t.var) (((EVAR e.something))) e.expr>;
//        };
//      } :: e.expr,
//      (e.expr) e.rest;
//  } :: (e.expr) e.vars,
//  e.vars : /*empty*/ =
//  e.expr;
//
//Left-Exp s.left s.len e.expr, \{
//  <"<" (<Min-Length e.expr>) (<"+" s.left s.len>)>
//    = $fail;
//  s.len : 0 = ();
//  s.left : 0 =
//    0 () e.expr $iter \{
//      e.expr : t1 e2, t1 : {
//        s.ObjectSymbol = <"+" s.num 1>;
////        (REF t.name) = ???
//        (PAREN e) = <"+" s.num 1> ;
//        (s.var-tag s.n (s.n) e.var-id) = <"+" s.num s.n>;
//        (s.var-tag s.m (e.n) e.var-id) =
//          <"+" s.num s.m> :: s.num,
//          <"<=" (s.len) (s.num)>,
//          s.num;
//      } :: s.num,
//        s.num (e.left t1) e2;
//    } :: s.num (e.left) e.expr,
//    <"<=" (s.len) (s.num)> =
//    <"-" s.num s.len> :: s.r-min,
//    e.left : e.first t.var,
//    t.var : {
//      s.ObjectSymbol = (e.left);
//      (PAREN e) = (e.left);
//      (s.tag s.m (e.n) e.NEW (e.QualifiedName)) = 
//        <"-" s.m s.r-min> :: s.l-len,
//        e.n : {
//          /*empty*/ = /*empty*/;
//          s.x = <"-" <"+" s.x <Min-Length e.first>> s.l-len>;
//        } : {
//          0 = (e.left);
//          e.r-max,
//            (s.tag s.l-len (s.l-len) NEW ("l-split" e.QualifiedName))
//              :: t.l-var,
//            (s.tag s.r-min (e.r-max) NEW ("r-split" e.QualifiedName))
//              :: t.r-var,
//            <Subst (t.var) ((t.l-var t.r-var)) e.first> :: e.expr,
//            (e.expr t.l-var) t.var t.l-var t.r-var;
//        };
//    };
//  <Left-Exp 0 s.left e.expr> :: (e.left) e.change,
//    {
//      e.change : t.old-var t.new-1 t.new-2 =
//        <Subst (t.old-var) ((t.new-1 t.new-2)) e.expr>;
//      e.expr;
//    } : e.left e.right,
//    <Left-Exp 0 s.len e.right> e.change;
//};
//
//Right-Exp s.right s.len e.expr, \{
//  <"<" (<Min-Length e.expr>) (<"+" s.right s.len>)>
//    = $fail;
//  s.len : 0 = ();
//  s.right : 0 =
//    0 () e.expr $iter \{
//      e.expr : e2 t1, t1 : {
//        s.ObjectSymbol = <"+" s.num 1>;
////        (REF t.name) = ???
//        (PAREN e) = <"+" s.num 1> ;
//        (s.var-tag s.n (s.n) e.var-id) = <"+" s.num s.n>;
//        (s.var-tag s.m (e.n) e.var-id) =
//          <"+" s.num s.m> :: s.num,
//          <"<=" (s.len) (s.num)>,
//          s.num;
//      } :: s.num,
//        s.num (t1 e.right) e2;
//    } :: s.num (e.right) e.expr,
//    <"<=" (s.len) (s.num)> =
//    <"-" s.num s.len> :: s.l-min,
//    e.right : t.var e.last,
//    t.var : {
//      s.ObjectSymbol = (e.right);
//      (PAREN e) = (e.right);
//      (s.tag s.m (e.n) e.NEW (e.QualifiedName)) = 
//        <"-" s.m s.l-min> :: s.r-len,
//        e.n : {
//          /*empty*/ = /*empty*/;
//          s.x = <"-" <"+" s.x <Min-Length e.last>> s.r-len>;
//        } : {
//          0 = (e.right);
//          e.l-max,
//            (s.tag s.r-len (s.r-len) NEW ("r-split" e.QualifiedName))
//              :: t.r-var,
//            (s.tag s.l-min (e.l-max) NEW ("l-split" e.QualifiedName))
//              :: t.l-var,
//            <Subst (t.var) ((t.l-var t.r-var)) e.last> :: e.expr,
//            (e.expr t.r-var) t.var t.l-var t.r-var;
//        };
//    };
//  <Right-Exp 0 s.right e.expr> :: (e.right) e.change,
//    {
//      e.change : t.old-var t.new-1 t.new-2 =
//        <Subst (t.old-var) ((t.new-1 t.new-2)) e.expr>;
//      e.expr;
//    } : e.left e.right,
//    <Right-Exp 0 s.len e.left> e.change;
//};
//
////  Right-Exp s.right s.len e.expr =
////    <Min-Length e.expr> :: s.expr-len,
////    <"+" s.right s.len> :: s.sum,
////    \{
////      <"<" (s.expr-len) (s.sum)> = $fail;
////      <Left-Exp <"-" s.expr-len s.sum> s.len e.expr>;
////    };
//  
//Middle-Exp s.left s.right e.expr, \{
//  <"<" (<Min-Length e.expr>) (<"+" s.left s.right>)>
//    = $fail;
//  <Left-Exp 0 s.left e.expr> :: (e.left) e.l-change,
//    <Right-Exp 0 s.right e.expr> :: (e.right) e.r-change,
//    e.expr : e.left e.sought e.right,
//    (e.sought) e.l-change e.r-change;
//};