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

$use "rfpc";
$use "rfp_err";
$use "rfp_list";
$use "rfp_helper";
$use "rfp_check";
$use "rfp_as2as";
$use "rfp_format";

$use StdIO;
$use Table;
$use Box;
$use Arithm;
$use Access;
$use Compare;
$use Convert;
$use Class;
$use Apply;
$use Dos;

/*
 * Tables for storing $const'ant values and their lengthes.
 */
$table Const-Len;

/*
 * Table for storing object names.
 */
$table Objects;

/*
 * Table for storing referenced functions.
 */
$table Ref-To-Funcs;

/*
 * Box for storing function out format
 */
$box Out-Format;

/*
 * Box for storing names for function result variables
 */
$box Res-Vars;

/*
 * Following table is used by Gener-Label function for obtaining unical (for
 * certain function) label name.
 * e.Key ::= e.QualifiedName      (parameter given to Gener-Label)
 * e.Val ::= [Int]          (last index used with such e.QualifiedName)
 */
$table Labels;

//$box Var-Stack;
$table Vars-Tab;

$box Last-Re;

$box Greater-Ineqs;
$box Less-Ineqs;

$const New-Clash-Tags = Unknown-length Ties Check-symbols Dereference Compare;

$table Static-Exprs;

$func Compile (e.targets) (e.headers) e.Items = e.Compiled-Items (INTERFACE e.headers);

$func Del-Pragmas e.Sentence = e.Sentence;

$func Print-Pragma s.channel t.Pragma = ;

$func AS-To-Ref e.AS-Expr = e.Refal-Expr;

$func Length-of e.Re = e.length;

$func Ref-Len t.name = s.length;

$func? Hard-Exp? e.expr = ;

$func Comp-Func-Stubs = e.asail-funcs;

$func Parenthesize-Operators e.Snt = e.Snt;

//$func Paren-Op t.Op = t.Op;
$func Paren-Op e = e;

//$func Get-Hard ... = (e.hard) e.matchings;

$func Comp-Func s.tag t.name e.params-and-body = e.compiled-func;

$func Post-Comp (e.used-vars) e.comp-func = (e.used-vars) e.result-func;

$func Set-Drops (e.declared-exprs) e.comp-func = (e.declared-exprs) e.result-func;

$func Comp-Sentence e.Sentence = e.asail-sentence;

//$func? Not-Ref? t.var = ;
$func? Not-Ref? e = e;

//$func? Contents-First? e.list (t.item e) = ;
$func? Contents-First? e = e;

//$func Zip-With-Vars e.col-vars (t.var (e.Re)) =
//  (t.var (e.Re) (e.all-collapsed-vars-from-Re));
$func Zip-With-Vars e = e;

$func Comp-Ready-Formats e.collapses =
  e.compiled-assignments (e.rest-collapses) (e.used-aux-vars);

//$func? Empty-Varlist? (t.var t.Re (/*empty-var-list*/)) = ;
$func? Empty-Varlist? e = e;

//$func Remove-Independ e.independ (t.var t.Re (e.var-list)) =
//  (t.var t.Re (e.new-var-list));
$func Remove-Independ e = e;

//$func Get-Aux-Indexes (t (e.Re) t) = e.list-of-lists-of-aux-indexes;
$func Get-Aux-Indexes e = e;

//$func Get-Var-Index t.var = e.aux-index-or-empty;
$func Get-Var-Index e = e;

//$func Longest-Re e.collapses (t.var t.Re t.col-vars) = (t.var t.Re t.col-vars s.num);
$func Longest-Re e = e;

//$func Longest-Re-Value t.var (t.var1 t.Re (e.col-vars)) s.value = s.new-value;
$func Longest-Re-Value e = e;

//$func Next-Collaps e.collapses (t.var t.Re (e.col-vars) s.len) (t.sel-var t t s.sel-len) =
//  (t.new-sel-var t t s.new-sel-len);
$func Next-Collaps e = e;

//$func Var-To-Len e.collapses t.var = s.len;
$func Var-To-Len e = e;

//$func Create-Aux t.var t.aux-var (t.var1 (e.Re) (e.col-vars) s.num) = e.collaps-or-empty;
$func Create-Aux e = e;

//$func Del-Checks s.Vars t.var = ;
$func Del-Checks e = e;

$func Comp-Pattern t.Pattern e.Snt = e.asail-Snt;

$func? Without-Calls? e.Re = ;

$func Norm-Vars (e.vars) e.Snt = (e.vars) e.Snt;

//$func Old-Vars e.expr = e.expr;

//$func Find-Known-Lengths e.clashes = (e.known-len-clashes) e.clashes;

//$func? Known-Vars? e.vars = ;

$func Comp-Clashes (e.clashes) (e.Current-Snt) e.Other-Snts = e.asail-Snt;

$func? Find-Var-Length e.clashes = e.cond (e.clashes);

$func Update-Ties t.var e.clashes = e.clashes;

$func Known-Length-of e.expr = e.known-length (e.unknown-vars);

$func? Cyclic-Restrictions e.clashes = e.cond (e.clashes);

$func Cyclic-Min t.var = e.min;

$func? Cyclic-Max t.var = e.max;

$func? Check-Symbols e.clashes = e.cond (e.clashes) s.new?;

$func? Check-Ft t.Ft (e.pos) (e.right-pos) t.name s.dir = e.Ft-cond s.stop?;

$func? Dereference-Subexpr e.clashes = e.cond (e.clashes);

$func Compare-Subexpr e.clashes = e.cond (e.asserts) (e.clashes) s.new?;

$func Compare-Ft t.Ft = e.Ft-cond s;

$func? Get-Source e.clashes = e.cond (e.clashes);

$func Compose-Expr e.expr = e.compose (e.not-instantiated-vars) s.flat?;

$func? Comp-Cyclic e.clashes = e.cond (e.clashes) (e.fail);

$func Get-Subexprs e.vars = e.asail-decls;

$func Unknown-Vars e.expr = e.known-expr (e.unknown-vars);

$func Split-Hard-Left e.expr = e.hard;

$func Split-Hard-Right e.expr = e.hard;

$func Gener-Label e.QualifiedName = t.label;

$func Comp-Re e.Re (e.Snt) = e.asail-Snt;

//$func? Second-Empty? (t.var ()) = ;
$func? Second-Empty? e = e;

//$func? Good-Res-Var? (t.var (t.F-var)) = ;
$func? Good-Res-Var? e = e;

$func Comp-Calls e.Re = e.calls;

$func Store-Vars e.vars = e.vars;

$func Declare-Vars s.type e.vars = e.decls;

$func Instantiate-Vars e.vars = ;

$func Comp-Assigns (e.vars) e.expressions = e.assignments;

$func Get-Static-Exprs e.expr = e.expr (e.decls);

$func Get-Static-Var e.expr = e.var (e.decl);

$func Strip-STVE expr = expr;

$func Set-Var t.name (e.key) (e.val) = ;

RFP-Compile e.Items =
  { <Lookup &RFP-Options ITEMS>;; } :: e.targets,
  <Compile (e.targets) () e.Items> :: e.Items t.Interface,
  t.Interface (MODULE e.Items);

Compile (e.targets) (e.headers) e.Items, {
  e.Items : e 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)) =
        { s.link : EXPORT = (DECL-FUNC t.name);; } :: e.decl,
        (e.decl) <Comp-Func s.tag t.name <Del-Pragmas (e.in) (e.out) e.branch>>;
      t.item : (s.link CONST t.pragma (e.QualifiedName) e.expr) =
        (CONSTEXPR ("r" e.QualifiedName) <Del-Pragmas e.expr>) :: t.const-decl,
        {
          s.link : EXPORT = (t.const-decl) /*empty*/;
          () t.const-decl;
        };
    } :: (e.decl) e.item =
    e.item <Compile (e.targets) (e.headers e.decl) e.rest>;
  /*<Comp-Func-Stubs>*/ (INTERFACE e.headers);
};

Del-Pragmas {
  eL t.Item eR, t.Item : \{
    (PRAGMA e) = eL <Del-Pragmas eR>;
    (expr) = eL (<Del-Pragmas expr>) <Del-Pragmas eR>;
  };
  e1 = e1;
};

/*
 * For each referenced function generate a stub one with format e = e.
 */
Comp-Func-Stubs =
  <Domain &Ref-To-Funcs> () $iter {
    e.funcs : ((e.QualifiedName)) e.rest,
      (e.QualifiedName 0) :: t.Fname,
//      <Bind &Ref-To-Funcs ((e.QualifiedName)) (t.Fname)>,
//      {
//        <In-Table? &Fun? (e.QualifiedName)> =
//          <Bind &Back-Funcs (t.Fname) ()>;;
//      },
//      <Bind &Fin (t.Fname) ((EVAR))>,
//      <Bind &Fout (t.Fname) ((EVAR))>,
      <Lookup-Func (e.QualifiedName)> :: s.linkage s.tag t.pragma (e.Fin) (e.Fout),
      <Gener-Vars 0 (e.Fin) "stub"> :: e.He s,
      <Comp-Func s.tag t.Fname ((EVAR "arg" 1)) ((EVAR "res" 1))
        (LEFT e.He) (RESULT (CALL (e.QualifiedName) e.He))
      > :: e.asail,
      e.rest (e.asail-funcs e.asail);
  } :: e.funcs (e.asail-funcs),
  e.funcs : /*empty*/ =
  // Here is place to define expressions - references to stub functions.
  // Use &Ref-To-Funcs for that.
  e.asail-funcs;

Comp-Func s.tag t.name (e.in) (e.out) e.Sentence =
  <RFP-Clear-Table &Labels>,
  <RFP-Clear-Table &Static-Exprs>,
  <Store &Greater-Ineqs /*empty*/>,
  <Store &Less-Ineqs /*empty*/>,
  <RFP-Clear-Table &Var-Tags>,
  <RFP-Clear-Table &Vars-Tab>,
  <Ref-To-Var e.Sentence> :: e.Sentence,
  <Store-Vars <Vars e.out>> :: e.res-vars,
  <Store &Res-Vars e.res-vars>,
  <Store &Out-Format <Format-Exp e.out>>,
  <Norm-Vars (<Vars e.in>) e.Sentence> :: (e.arg-vars) e.Sentence,
  <Declare-Vars Expr e.arg-vars> : e,
  <Instantiate-Vars e.arg-vars>,
  <Store &Last-Re /*empty*/>,
  s.tag : {
    FUNC = (Comp Fatal);
    FUNC? = (Comp Retfail);
  } :: t.retfail,
  (FUNC t.name (e.arg-vars) (e.res-vars)
      <Comp-Sentence () e.Sentence (Comp Sentence) t.retfail>
  ) :: e.comp-func,
  <Set-Drops () e.comp-func> :: t e.comp-func,
  <Post-Comp (e.res-vars) e.comp-func> :: t e.result,
  e.result;
//  :: (e.func-decl) e.func-body,
//  () <Domain &Declarations> $iter {
//    e.vars : (t.var) e.rest-vars,
//      (e.var-decls (DECL t.var)) e.rest-vars;
//  } :: (e.var-decls) e.vars,
//  e.vars : /*empty*/,
//  (e.func-decl e.var-decls e.func-body);

Ref-To-Var e.Snt =
  () e.Snt $iter {
    e.Snt : t.Statement e.rest, t.Statement : {
      (REF (e.QualifiedName)) =
        ("r" e.QualifiedName) :: t.name,
        <Table> :: s.tab,
        <Bind &Vars-Tab (t.name) (s.tab)>,
        <Set-Var t.name (Format) (<Format-Exp (REF (e.QualifiedName))>)>,
        <Set-Var t.name (Declared) (True)>,
        <Set-Var t.name (Instantiated) (True)>,
        <Set-Var t.name (Left-compare) ()>,
        <Set-Var t.name (Right-compare) ()>,
        <Set-Var t.name (Left-checks) ()>,
        <Set-Var t.name (Right-checks) ()>,
        (e.new-Snt (VAR t.name)) e.rest;
      (e.expr) = (e.new-Snt (<Ref-To-Var e.expr>)) e.rest;
      t = (e.new-Snt t.Statement) e.rest;
    };
  } :: (e.new-Snt) e.Snt,
  e.Snt : /*empty*/ =
  e.new-Snt;

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 (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 (e.yet-not-used) e.something e.statements>;
    <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 (<Or (e.used-vars) e.expr>) e.something> (e.expr);
  e.something s.symbol = <Post-Comp (e.used-vars) e.something> s.symbol;
  /*empty*/ = (e.used-vars);
};

Set-Drops (e.declared) e.comp-func =
  e.comp-func () (e.declared) $iter {
    e.comp-func : t.first e.rest, {
      t.first : \{
        (EXPR t.var e) = (DROP t.var) (t.first) t.var Init;
        (DEREF t.var e) = (DROP t.var) (t.first) t.var Init;
        (SUBEXPR t.var e) = (DROP t.var) (t.first) t.var Init;
        (DECL Expr t.var) = (DROP t.var) () t.var Decl;
        (DECL "int" t.var) = /*empty*/ () t.var Decl;
      } :: e.drop (e.constr) t.var s.init,
        {
          e.declared : e1 t.var s.old-init e2, s.old-init : {
            Init, {
              t.var : (VAR ("const" e)) =
                e.rest (e.result-func) (e.declared);
              e.rest (e.result-func e.drop e.constr) (e.declared);
            };
            Decl, s.init : {
              Decl =
                e.rest (e.result-func) (e.declared);
              Init =
                t.first : (s.method t.var e.args),
                e.rest (e.result-func (ASSIGN t.var (s.method e.args)))
                (e1 e2 t.var s.init);
            };
          };
          e.rest (e.result-func t.first) (e.declared t.var s.init);
        };
      t.first : (LABEL t.label e.expr) =
        <Set-Drops (e.declared) e.expr> :: (e.declared) e.expr,
        e.rest (e.result-func (LABEL t.label e.expr)) (e.declared);
      t.first : (e.expr) =
        <Set-Drops (e.declared) e.expr> :: t e.expr,
        e.rest (e.result-func (e.expr)) (e.declared);
      t.first : s.symbol =
        e.rest (e.result-func s.symbol) (e.declared);
    };
  } :: e.comp-func (e.result-func) (e.declared),
  e.comp-func : /*empty*/ =
  (e.declared) e.result-func;

Comp-Sentence (e.cuts) e.Sentence =
//  <WriteLN Snt e.Sentence>,
//  <WriteLN Last-Re <? &Last-Re>>,
//  <WriteLN Vars <Domain &Vars-Tab>>,
//  {
//    <Domain &Vars-Tab> : e (t.name) e,
//      <WriteLN '  ' t.name>,
//      {
//        <Lookup &Vars-Tab t.name> : s.tab,
//          <WriteLN '      ' s.tab>,
//          <Domain s.tab> : e (e.field) e,
//          <WriteLN '      ' e.field ':' <?? t.name e.field>>,
//          $fail;;
//      }, $fail;;
//  },
//  <WriteLN Greater-Ineqs <? &Greater-Ineqs>>,
//  <WriteLN Less-Ineqs <? &Less-Ineqs>>,
//  <WriteLN Static-Exprs <Domain &Static-Exprs>>,
//  <WriteLN Var-Tags <Domain &Var-Tags>>,
//  <WriteLN Cuts e.cuts>,
  e.Sentence : {
    (Comp Cut) e.Snt =
      <Comp-Sentence (e.cuts Cut) e.Snt>;
    t.Statement e.Snt =
      \{
        e.cuts : /*empty*/ = t.Statement : \{
          (Comp Empty) = /*empty*/;
          (Comp Used e.vars) =
            (Used e.vars) <Comp-Sentence () e.Snt>;
          (Comp Notail) =
            <Comp-Sentence () e.Snt>;
          (Comp Trap) =
            <Comp-Sentence () e.Snt>;
          (Comp Vars e.Preserve-Re? s.Vars-Tab s.Static (e.greater) (e.less)) = 
            <Store &Greater-Ineqs e.greater>,
            <Store &Less-Ineqs e.less>,
            <RFP-Double-Copy s.Vars-Tab> :: s.tmp-Tab,
            {
              e.Preserve-Re? : Preserve-Re =
                <Nub <Vars <? &Last-Re>>> $iter {
                  e.vars : (VAR t.name) e.rest,
                    <Lookup &Vars-Tab t.name> : s.tab,
                    <Table-Copy s.tab> :: s.new-tab,
                    <Bind s.tmp-Tab (t.name) (s.new-tab)>,
                    e.rest;
                } :: e.vars,
                e.vars : /*empty*/;;
            },
            <Replace-Table &Vars-Tab s.tmp-Tab>,
            <Replace-Table &Static-Exprs s.Static>,
            <Comp-Sentence () e.Snt>;
          (Comp Re e.Re) =
            <Store &Last-Re e.Re>,
            <Comp-Sentence () e.Snt>;
          (Comp Fatal) = FATAL;
          (Comp Retfail) = RETFAIL;
          (Comp Sentence) = RETURN;
          (Comp Not) =
            e.Snt : (Comp Sentence) e.Current (Comp Sentence) e.Others =
            <Comp-Sentence () e.Others>;
          (Comp Continue t.label) = (CONTINUE t.label);
          (Comp Break t.label) = (BREAK t.label);
          (Comp Error) =
            <Get-Static-Exprs <? &Last-Re>> :: e.Re (e.decls),
            e.decls (ERROR e.Re);
          (Comp Remove-next-sentence) =
            e.Snt : e.Curr-Snt (Comp Sentence)
                e.Next-Snt (Comp Sentence) e.Other-Snts,
            <Comp-Sentence () e.Curr-Snt (Comp Sentence) e.Other-Snts>;
          (Comp Cutall) =
            e.Snt : {
              e.Snt1 (Comp Not) e (Comp Sentence) e.Rest,
                {
                  e.Snt1 : e (Comp Notail) e (Comp Sentence)
                  e (Comp Sentence) e.Rest1 =
                    e.Rest1;
                  e.Rest;
                } :: e.Rest =
                <Comp-Sentence () e.Rest>;
              e (Comp Notail) e (Comp Sentence) e (Comp Sentence) e.Rest =
                <Comp-Sentence () e.Rest>;
              e t.retfail =
                <Comp-Sentence () t.retfail>;
            };
          (Comp Stake) =
            <Comp-Sentence () e.Snt>;
          (RESULT e.Re) =
            <Comp-Re e.Re (e.Snt)>;
          (FORMAT e.Hard) =
            <Norm-Vars (<Nub <Vars e.Hard>>) e.Snt> :: (e.vars) e.Snt,
            <Filter &Not-Ref? (e.vars)> :: e.vars,
            <? &Last-Re> :: e.Re,
            <Split-Re (<Format-Exp e.Hard>) e.Re> :: e.splited-Re,
            <Split &Contents-First? <Vars e.Re>
              (<Zip (e.vars) (e.splited-Re)>)> :: (e.collapses) (e.normals),
            /* Each var in e.collapses is presented in at least one
             * of Re from e.collapses and e.normals. And any var
             * from e.normals isn't contented in any Re at all. So
             * we can compute e.normals in the end - we can't get
             * much use of them anyway.
             */
            <Map &Get-Elem 0 (e.collapses)> :: e.collaps-vars,
            <Map &Zip-With-Vars e.collaps-vars (e.collapses)> :: e.collapses,
            /*
             * Now each "collaps" has the following structure:
             *  t.var (e.Re) (e.all-collapsed-vars-from-Re)
             * And e.all-collapsed-vars-from-Re does NOT contain t.var.
             */
            <Comp-Ready-Formats e.collapses> $iter {
              <Map &Longest-Re e.collapses (e.collapses)> :: e.collapses,
                /*
                 * Now each "collaps" has the following structure:
                 *  t.var (e.Re) (e.vars) s.num
                 * where s.num is maximum number of callapsed
                 * vars which including t.var are needed for
                 * computing some variable.
                 *  Next function chooses t.var with minimized
                 * maximum of all used in it variable's s.num.
                 */
                <Foldr1 &Next-Collaps e.collapses (e.collapses)>
                  : (t.next-var (e.next-Re) e),
                /*
                 * Choose free number for auxiliary variable index.
                 */
                1 e.aux $iter {
                  e.aux : e s.ind e = <"+" s.ind 1> e.aux;
                  s.ind /*empty*/;
                } :: s.ind e.aux,
                e.aux : /*empty*/ =
                <Store-Vars (EVAR ("aux" s.ind))> : t.aux-var,
                /*
                 * Create-Aux changes all t.var to t.aux-var and
                 * removes s.num from the end of collaps.
                 */
                e.comp-formats
                <Declare-Vars "Expr" t.aux-var>
                <Comp-Ready-Formats
                  (t.aux-var (t.next-var) ())
                  (t.next-var (e.next-Re) ())
                  <Map &Create-Aux t.next-var t.aux-var (e.collapses)>>;
            } :: e.comp-formats (e.collapses) (e.aux),
            e.collapses : /*empty*/ =
            <Map &Get-Elem 0 (e.normals)> :: e.normal-vars,
            e.comp-formats
            /*
             * Wouldn't be constructor in the form Expr(const_expr)
             * better?
             */
            <Declare-Vars "Expr" e.normal-vars>
            <Comp-Assigns (e.normal-vars) <Map &Get-Elem 1 (e.normals)>>
            <Comp-Sentence () e.Snt>;
          (STAKE) =
            e.Snt : e.Current (Comp Sentence) e.Others =
            <Comp-Sentence () e.Current (Comp Sentence) (Comp Stake) e.Others>;
          (CUT) = 
            e.Snt : e.Current (Comp Sentence) e.Others =
            <Comp-Sentence () e.Current (Comp Sentence) (Comp Cut) e.Others>;
          (CUTALL) =
            e.Snt : e.Current (Comp Sentence) e.Others =
            {
              e.Current : e1 (Comp Remove-next-sentence) e2 (Comp Notail) e3 =
                e.Others : e (Comp Sentence) e.rest,
                e1 e2 (Comp Notail) e3 :: e.Current,
                e.Current (Comp Sentence) e.rest;
              e.Current (Comp Sentence) (Comp Cutall) e.Others;
            } :: e.Snt,
            <Comp-Sentence () e.Snt>;
          (FAIL) =
            e.Snt : e.Current (Comp Sentence) e.Others =
            <Comp-Sentence () e.Others>;
          (NOT (BRANCH e.Snt1)) =
            <RFP-Double-Copy &Vars-Tab> :: s.Vars-Tab,
            <Table-Copy &Static-Exprs> :: s.Static,
            <? &Greater-Ineqs> :: e.greater,
            <? &Less-Ineqs> :: e.less,
            <Comp-Sentence () e.Snt1
              (Comp Not) (Comp Sentence) (RESULT)
              (Comp Vars s.Vars-Tab s.Static (e.greater) (e.less)) e.Snt>;
            //  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ?????????
          (LEFT e.Pattern) =
            <Comp-Pattern (LEFT e.Pattern) e.Snt>;
          (RIGHT e.Pattern) =
            <Comp-Pattern (RIGHT e.Pattern) e.Snt>;
          (Comp Source s.Vars-Tab s.Static t.NOFAIL e.next-terms) = e.Snt : {
            (BLOCK) e.Snt1 = 
              {
                t.NOFAIL : (Nofail) = FATAL;
                e.Snt : e.Current (Comp Sentence) e.Others =
                  <Comp-Sentence () e.Others>;
              };
            (BLOCK (BRANCH e.Branch) e.Branches) e.Snt1 =
              <? &Last-Re> :: e.Re,
              <? &Greater-Ineqs> :: e.greater,
              <? &Less-Ineqs> :: e.less,
              <Gener-Label L "Branch"> :: t.label,
              (LABEL t.label
              <Comp-Sentence () 
                (Comp Vars s.Vars-Tab s.Static (e.greater) (e.less))
                e.Branch e.next-terms
                (Comp Sentence) (Comp Break t.label)
                (Comp Source t.NOFAIL) e.Snt1>
              ) <Comp-Sentence ()
                (Comp Re e.Re)
                (Comp Source s.Vars-Tab s.Static t.NOFAIL e.next-terms)
                (BLOCK e.Branches) e.Snt1>;
          };
          NOFAIL =
            e.Snt : (BLOCK e.Branches) e.rest-Snt,
            <Comp-Sentence () (BLOCK (Nofail) e.Branches) e.rest-Snt>;
          (BLOCK) =
            <Comp-Sentence () (BLOCK ()) e.Snt>;
          (BLOCK (BRANCH e.Branch) e.Branches) =
            <Comp-Sentence () (BLOCK () (BRANCH e.Branch) e.Branches) e.Snt>;
          (BLOCK t.NOFAIL e.Branches) =
            /*
             * First of all remove form the begining of e.Snt
             * auxiliary terms (Comp...).
             */
            () e.Snt $iter {
              e.Snt : t.first e.rest =
                (e.comp-terms t.first) e.rest;
            } :: (e.comp-terms) e.Snt,
            # \{
              e.Snt : (Comp Vars e) e;
              e.Snt : (Comp Remove-next-sentence) e;
            } =
//            {
//              e.Snt : /*empty*/ = () e.comp-terms;
//              (e.comp-terms) e.Snt;
//            } :: (e.comp-terms) e.Snt,
            {
              e.Snt : (ITER t.body t.format t.cond) e.rest =
                t.format (ITER Comp t.body t.format t.cond) e.rest;
              e.Snt;
            } :: e.Snt,
            e.Snt : t.first e.rest, {
              t.first : \{
                (LEFT e.pattern) = e.pattern;
                (RIGHT e.pattern) = e.pattern;
                (FORMAT e.format) = e.format;
              } :: e.expr =
                <Norm-Vars (<Vars e.expr>) e.Snt> : (e.vars) t.f e.r,
                (<Declare-Vars "Expr" e.vars>) (t.f) e.r;
              () () e.Snt;
            } :: (e.decls) (e.next-term) e.Snt,
            e.Snt : e.Curr-Snt (Comp Sentence) e =
            {
              e.next-term : t1, {
                e.comp-terms : /*empty*/ =
                  t1 (Comp Notail) (Preserve-Re);
                t1 (Preserve-Re);
              };
              e.Curr-Snt : e t.item e,
                # \{ t.item : (Comp e); } = 
                (Comp Notail) (Preserve-Re);
              /*empty*/ ();
            } :: e.next-terms (e.pres-Re),
            { e.next-term : (s e.nt) = e.nt; /*empty*/; } :: e.next-term,
            <RFP-Double-Copy &Vars-Tab> :: s.Vars-Tab, // ?????????
            <Table-Copy &Static-Exprs> :: s.Static,
            {
              e.comp-terms : /*empty*/ =
                <? &Greater-Ineqs> :: e.greater,
                <? &Less-Ineqs> :: e.less,
                (Comp Vars e.pres-Re s.Vars-Tab s.Static (e.greater) (e.less))
                (Comp Remove-next-sentence) e.next-terms;
              e.comp-terms e.next-terms;
            } :: e.next-terms,
            <Gener-Label L "Block"> :: t.label,
            e.decls
            (LABEL t.label
              <Comp-Sentence ()
                (Comp Source s.Vars-Tab s.Static t.NOFAIL e.next-terms
                (Comp Break t.label)) (BLOCK e.Branches) e.Snt>
            ) <Comp-Sentence ()
              (Comp Re e.next-term)
              (Comp Vars Preserve-Re s.Vars-Tab s.Static (/*???*/) (/*???*/))
              (Comp Empty)> :: e.tmp-Snt,
            <Foldr &Del-Checks s.Vars-Tab () (<Nub <Vars e.next-term>>)> : e =
            e.tmp-Snt <Comp-Sentence () e.Snt>;
          (ITER e.Comp t (FORMAT e.Hard) t) =
            <Norm-Vars (<Vars e.Hard>) t.Statement e.Snt> :
              (e.vars)
              (ITER e (BRANCH e.IterBody) t.Format (BRANCH e.IterCondition))
              e.Current-Snt (Comp Sentence) e.Other-Snts,
            {
              e.Comp : Comp = /*empty*/;
              <Comp-Sentence () t.Format (Comp Empty)>;
            } :: e.init,
            <Gener-Label L "Iter"> :: t.label,
            <RFP-Double-Unbind &Vars-Tab <Map &Get-Elem 1 (e.vars)>>,
            <Declare-Vars "Expr" e.vars> : e,
            <Instantiate-Vars e.vars>,
            <RFP-Double-Copy &Vars-Tab> :: s.Vars-Tab,
            <Comp-Sentence () e.IterCondition e.Current-Snt
              (Comp Sentence) (Comp Break t.label) e.Other-Snts> :: e.cond,
            <Replace-Table &Vars-Tab s.Vars-Tab>,
            <Comp-Sentence () e.IterBody t.Format (Comp Used e.vars)
              (Comp Empty) (Comp Sentence) e.Other-Snts> :: e.body,
            e.init (FOR () () () (LABEL t.label e.cond) e.body);
          (TRY (BRANCH e.TrySnt) e.CatchBlock) =
            <RFP-Double-Copy &Vars-Tab> :: s.Vars-Tab,
            e.Snt : e.Current-Snt (Comp Sentence) e,
            e.Current-Snt : {
              e1 (Comp Remove-next-sentence) e2 = e1 e2;
              e.Current-Snt;
            } :: e.Current-Snt,
            <Comp-Sentence () e.TrySnt e.Current-Snt
              (Comp Trap) (Comp Sentence) (Comp Fatal)> :: e.try,
            <Replace-Table &Vars-Tab s.Vars-Tab>,
            <Store-Vars (EVAR ("err" 0))> : t.err,
            <Declare-Vars "Expr" t.err> : e,
            <Instantiate-Vars t.err>,
            <Comp-Sentence () (Comp Re t.err) e.CatchBlock e.Snt> :: e.catch,
            (TRY e.try) (CATCH-ERROR e.catch);
          t.error, t.error : (ERROR) =  // Due to the bug in ver. 1.8.7
            e.Snt : e.Current-Snt (Comp Sentence) e,
            e.Current-Snt : $r e.CurrSnt (RESULT e.Re) e,
            <Comp-Sentence () e.CurrSnt (RESULT e.Re) (Comp Error)
              (Comp Sentence) (Comp Fatal)>;
        };
        e.cuts : e.cuts1 Cut = \{
          t.Statement : (Comp Stake) =
            <Comp-Sentence (e.cuts1) e.Snt>;
          <Comp-Sentence (e.cuts) e.Snt>;
        };
      };
  };

Not-Ref? (VAR t.name) = # \{ <?? t.name Format> : (REF e); };

Contents-First? e.list (t.item e) = e.list : e t.item e;

Zip-With-Vars e.col-vars (t.var (e.Re)) =
  (t.var (e.Re) (<Sub (<Filter &Elem? e.col-vars (<Nub <Vars e.Re>>)>) t.var>));

/*
 * Finds all vars independent from collapsed ones and computes assignments to
 * them. Also returns new list of collapsed varibles and indexes of binded
 * auxiliary variables.
 */
Comp-Ready-Formats e.collapses =
  <Split &Empty-Varlist? (e.collapses)> :: (e.independ) (e.collapses),
  <Map &Get-Elem 0 (e.independ)> :: e.indep-vars,
  <Map &Remove-Independ e.indep-vars (e.collapses)> :: e.collapses,
  <Comp-Assigns (e.indep-vars) <Map &Get-Elem 1 (e.independ)>>
  (e.collapses)
  (<Concat <Map &Get-Aux-Indexes (e.collapses)>>);

Empty-Varlist? (t.var t.Re (/*empty-var-list*/)) = ;

Remove-Independ e.independ (t.var t.Re (e.var-list)) =
  (t.var t.Re (<Sub (e.var-list) e.independ>));

Get-Aux-Indexes (t (e.Re) t) = <Map &Get-Var-Index (<Nub <Vars e.Re>>)>;

Get-Var-Index {
  (VAR ("aux" s.ind)) = s.ind;
  t.var = /*empty*/;
};

Longest-Re e.collapses (t.var t.Re t.col-vars) =
  (t.var t.Re t.col-vars <Foldr &Longest-Re-Value t.var (0) (e.collapses)>);

Longest-Re-Value t.var (t.var1 t.Re (e.col-vars)) s.value, {
  <Length e.col-vars> :: s.len,
    <">" (s.len) (s.value)>, e.col-vars : e t.var e = s.len;
  s.value;
};

Next-Collaps e.collapses (t.var t.Re (e.col-vars) s.len) (t.sel-var t.sel-Re t s.sel-len) =
  <Foldr1 &Max (<Map &Var-To-Len e.collapses (e.col-vars)>)> : s.new-len,
  {
    <"<" (s.new-len) (s.sel-len)> = (t.var t.Re () s.new-len);
    (t.sel-var t.sel-Re () s.sel-len);
  };

Var-To-Len e.collapses t.var =
  e.collapses : e (t.var t t s.len) e = s.len;

Create-Aux t.var t.aux-var (t.var1 (e.Re) (e.col-vars) s), {
  t.var : t.var1 = /*empty*/;
  (t.var1 (<Subst (t.var) ((t.aux-var)) e.Re>) (<Sub (e.col-vars) t.var>));
};

Del-Checks s.Vars (VAR t.name), {
  <Lookup s.Vars t.name> : s.tab =
    {
      Left-compare Right-compare Left-checks Right-checks : e s.field e,
        <Set-Var t.name (s.field) (<Lookup s.tab s.field>)>,
        $fail;;
    };
  <Set-Var t.name (Format) ((VAR t.name))>,
    {
      Left-compare Right-compare Left-checks Right-checks : e s.field e,
        <Set-Var t.name (s.field) ()>,
        $fail;;
    };
};

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>;
  };

Without-Calls? e.Re =
  e.Re $iter \{
    e.Re : t.Rt e.rest,
      t.Rt : \{
        (CALL e) = $fail;
        (BLOCK e) = $fail;
        (PAREN e.Re1) = <Without-Calls? e.Re1>;
        t.symbol-or-var = /*empty*/;
      },
      e.rest;
  } :: e.Re,
  e.Re : /*empty*/;

Norm-Vars (e.vars) e.Snt =
  /*
   * Store all new variables in the &Vars-Tab table and return the list with
   * all variables in the (VAR t.name) form.
   */
  <Store-Vars e.vars> :: e.new-vars,
  /*
   * Rename all new variables in e.Snt. Never mind multiple occurences.
   */
  (e.vars) (e.new-vars) e.Snt $iter {
    e.vars : t.var e.rest, e.tmp-vars : t.new-var e.new-rest, {
      t.var : t.new-var =
        (e.rest) (e.new-rest) e.Snt;
      t.var : (s.tag e),
        <Bind &Var-Tags (t.new-var) (s.tag)>,
        (e.rest) (e.new-rest) <Subst (t.var) ((t.new-var)) e.Snt>;
    };
  } :: (e.vars) (e.tmp-vars) e.Snt,
  e.vars : /*empty*/ =
  (e.new-vars) e.Snt;

//Comp-Clashes (e.clashes) (e.Current-Snt) e.Other-Snts =
//  <WriteLN Clashes e.clashes>,
////  /*
////   * Collect in e.vars all varibles from all clashes.
////   */
////  () e.clashes $iter {
////    e.not-watched : (e.expr) e.rest = (e.vars <Vars e.expr>) e.rest;
////  } :: (e.vars) e.not-watched,
////  e.not-watched : /*empty*/ =
////  /*
////   * Rename all collected variables in all clashes. Never mind multiple
////   * occurences.
////   */
////  (e.clashes) e.vars $iter {
////    e.vars : (s.var-tag s.m (e.n) e.var-id) e.rest, {
////      <Known-Vars? (s.var-tag e.var-id)> =
////        e.var-id : e.NEW (e.QualifiedName),
////        <Subst ((s.var-tag s.m (e.n) e.var-id))
////          (((s.var-tag (s.var-tag NEW ("len" e.QualifiedName))
////          s.m (e.n) e.var-id))) e.clashes>;
////      s.m : e.n =
////        <Subst ((s.var-tag s.m (e.n) e.var-id))
////          (((s.var-tag (s.m) s.m (e.n) e.var-id))) e.clashes>;
////    } :: e.clashes,
////    (e.clashes) e.rest;
////  } :: (e.clashes) e.vars,
////  e.vars : /*empty*/ =
////  /*
////   * Now all variables with known length have ref. term after s.var-tag.
////   * Well, lets see if there are closed variables and compute their lengthes
////   * too.
////   */
////  e.clashes (e.clashes) () $iter {
////    e.not-watched : (e.Re) (s.dir e.Pe) e.rest, {
////      <Find-Closed-Var e.Pe> :: t.old-var t.new-var e.new-cond,
////        <Subst (t.old-var) ((t.new-var)) e.clashes> :: e.clashes,
////        e.clashes (e.clashes) (e.cond e.new-cond);
////      e.rest (e.clashes) (e.cond);
////    };
////  } :: e.not-watched (e.clashes) (e.cond),
////  e.not-watched : /*empty*/ =
//
//  /*
//   * Parenthesize each clash, so from now on they can be seen as a sequence
//   * of such terms: (e.temp-tags (e.Re) t.P)
//   */
//  e.clashes () $iter {
//    e.old-clashes : t.R t.P e.rest =
//      e.rest (e.clashes (t.R t.P));
//  } :: e.old-clashes e.clashes,
//  e.old-clashes : /*empty*/ =
//  
//  <Find-Known-Lengths e.clashes> :: (e.known-len-clashes) e.clashes,
//  {
//    e.known-len-clashes : /*empty*/ =
//      <Find-Symbol-Checks e.clashes> :: (e.sym-check-clashes) e.clashes,
//      {
//        e.sym-check-clashes : /*empty*/ =
//          e.clashes : {
//            (e.Re) (s.dir e.Pe) e.rest =
//              <Gener-Label L> :: t.label,
//              <Comp-Clashes (e.rest) (e.Current-Snt)
//                (Comp Continue t.label) e.Other-Snts>
//              :: e.asail-Snt,
//              (FOR t.label () () ()
//                e.asail-Snt
//              )
//              <Comp-Sentence () e.Other-Snts>;
//            /*empty*/ =
//              <Comp-Sentence () e.Current-Snt e.Other-Snts>;
//          };
//        <Comp-Clashes (e.clashes) (e.Current-Snt) e.Other-Snts> :: e.asail-Snt,
//          (e.sym-check-clashes) e.asail-Snt $iter {
//            e.sym-check-clashes : e.something (e (e.Re) (s.dir e.Pe)),
//              
//    <Comp-Clashes (e.clashes) (e.Current-Snt) e.Other-Snts> :: e.asail-Snt,
//      (e.known-len-clashes) e.asail-Snt $iter {
//        e.known-len-clashes : e.something (e.tags (e.Re) (s.dir e.Pe)),
//          (e.something)
//          (IF ((INFIX "==" (<Length-of e.Re>) (<Length-of e.Pe>)))
//            e.asail-Snt
//          );
//      } :: (e.known-len-clashes) e.asail-Snt,
//      e.known-len-clashes : /*empty*/ =
//      e.asail-Snt
//      <Comp-Sentence () e.Other-Snts>;
//  };
//
//Find-Known-Lengths e.clashes =
//  e.clashes () () $iter {
//    e.old-clashes : t.first e.rest, t.first : {
//      (e1 Known-length e2) =
//        e.rest (e.known) (e.clashes t.first);
//      (e.tags (e.Re) (s.dir e.Pe)) =
////        Known <Vars e.Re> <Vars e.Pe> $iter {
////          e.vars : (VAR t.name) e.rest-vars, {
////            <?? t.name Length> : e = Known;
////            <?? t.name Instantiated> : True = Known;
////            Unknown;
////          } :: s.known? =
////            s.known? e.rest-vars;
////        } :: s.known? e.vars,
////        \{
////          s.known? : Unknown =
////            e.rest (e.known) (e.clashes t.first);
////          e.vars : /*empty*/ =
////            e.rest (e.known t.first)
////            (e.clashes (e.tags Known-length (e.Re) (s.dir e.Pe)));
////        };
//        {
//          <Hard-Exp? <Vars e.Re> <Vars e.Pe>> =
//            e.rest (e.known t.first)
//            (e.clashes (e.tags Known-length (e.Re) (s.dir e.Pe)));
//          e.rest (e.known) (e.clashes t.first);
//        };
//    };
//  } :: e.old-clashes (e.known) (e.clashes),
//  e.old-clashes : /*empty*/ =
//  (e.known) e.clashes;
//
//Known-Vars? e.vars =
//  <? &Var-Stack> :: e.known-vars,
//  e.vars $iter {
//    e.vars : t.var e.rest =
//      e.known-vars : e t.var e,
//      e.rest;
//  } :: e.vars,
//  e.vars : /*empty*/;

Comp-Clashes (e.clashes) (e.Current-Snt) e.Other-Snts =
//  <WriteLN Clashes e.clashes>,
  /*
   * Parenthesize each clash, so from now on they can be seen as a sequence
   * of such terms: (e.temp-tags (e.Re) t.P)
   */
  e.clashes () $iter {
    e.old-clashes : t.R t.P e.rest =
      e.rest (e.clashes (<Gener-Label "clash"> &New-Clash-Tags t.R t.P));
  } :: e.old-clashes (e.clashes),
  e.old-clashes : /*empty*/ =
  
  /*empty*/ (e.clashes) () $iter {
    /*
     * First of all see if we have a clash with all variables of known length
     * and without length conditions written out.
     */
    e.clashes : e1 (e.t1 Known-length e.t2 (e.Re) (s.dir e.Pe)) e2,
      <Hard-Exp? e.Re e.Pe> =
      e.cond
      (Cond IF ((INFIX "==" (<Length-of e.Re>) (<Length-of e.Pe>))))
      (e1 (e.t1 Checked-length e.t2 (e.Re) (s.dir e.Pe)) e2) (e.fail);
    /*
     * Next see if we can compute length of some variable.
     */
    e.cond <Find-Var-Length e.clashes> (e.fail);
    /*
     * Write out restrictions for the cyclic variables.
     */
    e.cond <Cyclic-Restrictions e.clashes> (e.fail);
//    <Cyclic-Restrictions e.clashes> :: e.new-cond (e.clashes),
//      {
//        e.fail : v = e.cond e.new-cond (Clear-Restricted) (e.clashes) (e.fail); 
//        e.cond e.new-cond (e.clashes) (e.fail);
//      };
    /*
     * After checking all possible lengthes at the upper level change
     * <<current_label_if_fail>>.
     */
    e.fail : v =
      (Contin e.fail) e.cond (Fail e.fail) (Clear-Restricted) (e.clashes) ();
    /*
     * For all clashes with known left part check unwatched terms whether they
     * are symbols or reference terms or not any.
     */
    \?
    {
      <Check-Symbols e.clashes> : {
        v.new-cond (e.new-clashes) s =
          e.cond (Cond IF (v.new-cond)) (e.new-clashes) ();
        (e.new-clashes) New = e.cond (e.new-clashes) ();
        e \! $fail;
      };
      <PrintLN "Check-Symbols: don't know what to do... ;-)">, $fail;
    };
    /*
     * And then try to compose new clash by dereferencing a part of some one.
     */
    e.cond <Dereference-Subexpr e.clashes> ();
    /*
     * If previous doesn't work then compare recursively all known
     * subexpressions and all unknown repeated subexpressions with
     * corresponding parts of source.
     */
    <Compare-Subexpr e.clashes> :: e.new-cond (e.asserts) (e.new-clashes) s.new?,
      \{
        e.new-cond : v, {
          e.asserts : v =
            e.cond (Assert e.asserts) (Cond IF (e.new-cond)) (e.new-clashes) ();
          e.cond (Cond IF (e.new-cond)) (e.new-clashes) ();
        };
        e.asserts : v = e.cond (Assert e.asserts) (e.new-clashes) ();
        s.new? : New = e.cond (e.new-clashes) ();
      };
    /*
     * Then get first uncatenated source and bring it to the normal
     * form, i.e. concatenate and parenthesize until it became single
     * known expression.
     */
    e.cond <Get-Source e.clashes> ();
    /*
     * Now it's time to deal with cycles.
     */
    e.cond <Comp-Cyclic e.clashes>;
    /*
     * At last initialize all new subexpressions from all clashes.
     */
    e.clashes () $iter {
      e.clashes : (e t.Re (s.dir e.Pe)) e.rest,
        e.rest (e.new-cond <Get-Subexprs <Vars e.Pe>>);
    } :: e.clashes (e.new-cond),
      e.clashes : /*empty*/ =
      {
        e.new-cond : /*empty*/ = e.cond () ();
        e.cond (Assert e.new-cond) () ();
      };
  } :: e.cond (e.clashes) (e.fail),
//  <WriteLN CC-Clashes e.clashes>,
//  <WriteLN CC-Cond e.cond>,
  e.clashes : /*empty*/ =

  e.cond () 0 $iter {
    e.cond : (Contin (CONTINUE t.label)) e.rest =
      e.rest (e.contin (Comp Continue t.label)) 0;
    e.cond (e.contin) 1;
  } :: e.cond (e.contin) s.stop?,
  s.stop? : 1 =
  <Comp-Sentence () e.Current-Snt e.contin e.Other-Snts> :: e.asail-Snt,
  e.cond (e.asail-Snt) () $iter {
    e.cond : e.some (e.last),
      e.last : {
        Cond e.condition =
          e.some ((e.condition e.asail-Snt)) (e.vars);
        Assert e.assertion =
          e.some (e.assertion e.asail-Snt) (e.vars);
        Fail e.fail1 =
          e.some (e.asail-Snt e.fail1) (e.vars);
        Restricted t.var =
          e.some (e.asail-Snt) (e.vars t.var);
        If-not-restricted t.var e.restr-cond, {
          e.vars : e t.var e = e.some (e.asail-Snt) (e.vars);
          e.some e.restr-cond (e.asail-Snt) (e.vars);
        };
        Clear-Restricted = e.some (e.asail-Snt) ();
      };
  } :: e.cond (e.asail-Snt) (e.vars),
  e.cond : /*empty*/ =
  e.asail-Snt/* <Comp-Sentence () e.Other-Snts>*/;

Find-Var-Length e.clashes =
//  <WriteLN Find-Var-Length e.clashes>,
  e.clashes : e1 (e.t1 Unknown-length e.t2 (e.Re) (s.dir e.Pe)) e2 \?
  <Unknown-Vars e.Pe> :: e.new-Pe (e.Pe-unknown),
  <Unknown-Vars e.Re> :: e.new-Re (e.Re-unknown),
//  <Write Unknown>, <Write (e.Re-unknown)>, <WriteLN (e.Pe-unknown)>,
  e.Re-unknown e.Pe-unknown : {
    /*empty*/ =
      (e1 (e.t1 Known-length e.t2 (e.Re) (s.dir e.Pe)) e2);
    (VAR t.name) e.rest,
      e.rest $iter \{
        e.unknown : (VAR t.name) e.rest1 = e.rest1;
      } :: e.unknown,
      e.unknown : /*empty*/,
      <"-" <Length e.Re-unknown> <Length e.Pe-unknown>> : {
        0 \! $fail;
        s.diff, {
          <"<" (s.diff) (0)> =
            <"*" s.diff -1>
            (INFIX "-" (<Length-of e.new-Re>) (<Length-of e.new-Pe>));
          <">" (s.diff) (0)> =
            s.diff
            (INFIX "-" (<Length-of e.new-Pe>) (<Length-of e.new-Re>));
        } :: s.mult e.diff,
          t.name : (e.QualifiedName),
          (VAR ("len" e.QualifiedName)) :: t.len-var,
          {
            <?? t.name Max> :: e.max =
              (INFIX "<=" 
                (t.len-var)
                ((INFIX "*" (s.mult) (e.max)))
              );
            /*empty*/;
          } :: e.cond,
          e.cond
          (INFIX ">=" 
            (t.len-var)
            ((INFIX "*" (s.mult) (<?? t.name Min>)))
          )
          (NOT (INFIX "%"
            (t.len-var)
            (s.mult)
          )) :: e.cond,
          <Set-Var t.name (Max) (//(LENGTH (VAR t.name))
            (INFIX "/" (t.len-var) (s.mult))
          )>,
          <Set-Var t.name (Min) (<?? t.name Max>)>,
          <Set-Var t.name (Length) (<?? t.name Max>)>,
//          <WriteLN Unknown-Num s.mult> =
          (Restricted (VAR t.name))
          (Assert
            <Declare-Vars "int" t.len-var>
            (ASSIGN t.len-var e.diff)
          )
          (Cond IF (e.cond))
          (<Update-Ties (VAR t.name) e1>
            (e.t1 Checked-length e.t2 (e.Re) (s.dir e.Pe))
          <Update-Ties (VAR t.name) e2>);
      };
    e.unknown \!
      e.t1 Unknown-length e.t2 : e.t3 Ties e.t4 =
      e.t1 : t.id e,
      e.unknown () $iter {
        e.unknown : (VAR t.name) e.rest, {
          e.tied : e (VAR t.name) e = e.rest (e.tied);
          <Entries (VAR t.name) (e.Re)> :: s.Re-ent e.new-Re,
            <Entries (VAR t.name) (e.Pe)> :: s.Pe-ent e.new-Pe,
            <"-" s.Re-ent s.Pe-ent> :: s.diff,
            {
              s.diff : 0 = e.rest (e.tied (VAR t.name));
              {
                <"<" (s.diff) (0)> =
                  <"*" s.diff -1> (e.new-Re) (e.new-Pe);
                s.diff (e.new-Pe) (e.new-Re);
              } :: s.diff (e.plus) (e.minus),
                (
                  t.id
                  (<Known-Length-of e.plus>)
                  (<Known-Length-of e.minus>)
                  s.diff
                ) :: t.tie,
                {
                  <?? t.name Ties> : {
                    e.c1 (t.id e) e.c2 = e.c1 e.c2;
                    e.ties = e.ties;
                  };
                  /*empty*/;
                } :: e.ties,
                {
                  e.ties : e t.tie e;
                  <Set-Var t.name (Ties) (e.ties t.tie)>;
                },
                e.rest (e.tied (VAR t.name));
            };
        };
      } :: e.unknown (e.tied),
      e.unknown : /*empty*/ =
      {
        e.t3 e.t4 : e Cyclic e = e.t3 e.t4;
        e.t3 e.t4 Cyclic;
      } :: e.tags,
      (e1 (e.tags (e.Re) (s.dir e.Pe)) e2);
  };

Known-Length-of e.expr =
  <Unknown-Vars e.expr> :: e.expr (e.vars),
  <Length-of e.expr> (e.vars);

Update-Ties t.var e.clashes =
  e.clashes () $iter {
    e.clashes : t.clash e.rest,
      t.clash : (e.tags (e.Re) (s.dir e.Pe)),
      {
        e.tags : e Ties e = e.rest (e.new-clashes t.clash);
        e.Re e.Pe : e t.var e =
          e.rest (e.new-clashes (e.tags Ties (e.Re) (s.dir e.Pe)));
        e.rest (e.new-clashes t.clash);
      };
  } :: e.clashes (e.new-clashes),
  e.clashes : /*empty*/ =
  e.new-clashes;

Cyclic-Restrictions e.clashes =
  e.clashes : e1 (e.t1 Cyclic e.t2 (e.Re) (s.dir e.Pe)) e2 =
  <Unknown-Vars e.Re e.Pe> :: e (e.unknown),
  e.unknown () $iter {
    e.unknown : t.var e.rest,
      t.var : (VAR (e.QualifiedName)),
      (VAR ("min" e.QualifiedName)) :: t.min-var,
      <Cyclic-Min t.var> :: e.min,
      {
        <Cyclic-Max t.var> :: e.max =
          e.rest (e.cond (Restricted t.var) (If-not-restricted t.var
            (Assert 
              <Declare-Vars "int" t.min-var> (ASSIGN t.min-var e.min)
            )
            (Cond IF ((INFIX "<=" (t.min-var) (e.max))))
        ));
        e.rest (e.cond);
      };
  } :: e.unknown (e.cond),
  e.unknown : /*empty*/ =
  e.cond (e1 (e.t1 e.t2 (e.Re) (s.dir e.Pe)) e2);

Cyclic-Min (VAR t.name) =
  <?? t.name Ties> () $iter {
    e.ties : (t (e.plus (e.plus-vars)) (e.minus (e.minus-vars)) s.mult) e.rest, {
      e.minus-vars () $iter \{
        e.minus-vars : t.var e.vars-rest,
          e.vars-rest (e.minus-maxes <Cyclic-Max t.var>);
      } :: e.minus-vars (e.minus-maxes),
        e.minus-vars : /*empty*/ =
        e.plus-vars () $iter {
          e.plus-vars : (VAR t.var-name) e.vars-rest =
            e.vars-rest (e.plus-mins <?? t.var-name Min>);
        } :: e.plus-vars (e.plus-mins),
        e.plus-vars : /*empty*/ =
        e.rest (e.mins ((INFIX "/"
          ((INFIX "-" (e.plus e.plus-mins) (e.minus e.minus-maxes))) (s.mult)
        )));
      e.rest (e.mins);
    };
  } :: e.ties (e.mins),
  e.ties : /*empty*/ =
  (<?? t.name Min>) e.mins :: e.mins,
  {
    e.mins : (e.min) = e.min;
    (MAX e.mins);
  };

Cyclic-Max (VAR t.name) =
  <?? t.name Ties> () $iter {
    e.ties : (t (e.plus (e.plus-vars)) (e.minus (e.minus-vars)) s.mult) e.rest, {
      e.plus-vars () $iter \{
        e.plus-vars : (VAR t.var-name) e.vars-rest,
          e.vars-rest (e.plus-maxes <?? t.var-name Max>);
      } :: e.plus-vars (e.plus-maxes),
        e.plus-vars : /*empty*/ =
        e.minus-vars () $iter {
          e.minus-vars : (VAR t.var-name) e.vars-rest =
            e.vars-rest (e.minus-mins <?? t.var-name Min>);
        } :: e.minus-vars (e.minus-mins),
        e.minus-vars : /*empty*/ =
        e.rest (e.maxes ((INFIX "/"
          ((INFIX "-" (e.plus e.plus-maxes) (e.minus e.minus-mins))) (s.mult)
        )));
      e.rest (e.maxes);
    };
  } :: e.ties (e.maxes),
  e.ties : /*empty*/ =
  {
    (<?? t.name Max>) e.maxes;
    e.maxes;
  } :: e.maxes,
  {
    e.maxes : /*empty*/ = $fail;
    e.maxes : (e.max) = e.max;
    (MIN e.maxes);
  };

Check-Symbols e.clashes =
  e.clashes () () Old $iter {
    e.clashes : t.clash e.rest, {
      t.clash : (e.t1 Check-symbols e.t2 (e.Re) (s.dir e.Pe)),
        e.Re : (VAR t.name),
        <?? t.name Instantiated> : True =
//        <Format e.Pe> () () Continue $iter {
        e.Pe () () Continue $iter {
          e.format : t.Ft e.Fe =
            <Length-of e.left> :: e.pos,
            <Check-Ft t.Ft (e.pos) (1 <Length-of e.Fe>) t.name Left-checks> : {
              /*empty*/ s.stop??? = /*empty*/ s.stop???;
              Sym s.stop??? =
                (Used e.Re) (SYMBOL? e.Re (e.pos)) s.stop???;
              Ref s.stop??? =
                (Used e.Re) (NOT (SYMBOL? e.Re (e.pos))) s.stop???;
              Flat e.len s.stop??? =
                (Used e.Re) (FLAT-SUBEXPR? e.Re (e.pos) (e.len)) s.stop???;
            } :: e.Ft-cond s.stop? =
            e.Fe (e.left t.Ft) (e.new-cond e.Ft-cond) s.stop?;
        } :: e.format (e.left) (e.new-cond) s.stop?,
        \{
          e.format : /*empty*/ =
            e.rest (e.cond e.new-cond)
            (e.new-clashes (e.t1 e.t2 (e.Re) (s.dir e.Pe))) New;
          s.stop? : Stop =
            e.format () (e.new-cond) Continue $iter {
              e.format : e.Fe t.Ft =
                1 <Length-of e.right> :: e.pos,
                <Check-Ft t.Ft (e.pos) () t.name Right-checks>
                  :: e.Ft-cond s.stop?,
                e.Ft-cond : {
                  /*empty*/ = /*empty*/;
                  Sym =
                    (Used e.Re)
                    (SYMBOL? e.Re (
                      (INFIX "-" (<Length-of e.Re>) (e.pos))
                    ));
                  Ref =
                    (Used e.Re)
                    (NOT (SYMBOL? e.Re (
                      (INFIX "-" (<Length-of e.Re>) (e.pos))
                    )));
                  Flat e.len s.stop??? =
                    (Used e.Re)
                    (FLAT-SUBEXPR? e.Re (
                      (INFIX "-" (<Length-of e.Re>) (e.pos))
                    ) e.len) s.stop???;
                } :: e.Ft-cond,
                e.Fe (t.Ft e.right) (e.new-cond e.Ft-cond) s.stop?;
            } :: e.format (e.right) (e.new-cond) s.stop?,
            s.stop? : Stop =
            e.rest (e.cond e.new-cond) (e.new-clashes t.clash) s.new?;
        };
      e.rest (e.cond) (e.new-clashes t.clash) s.new?;
    };
  } :: e.clashes (e.cond) (e.new-clashes) s.new?,
//  <WriteLN Check-Symbols e.clashes (e.cond) (e.new-clashes) s.new?>,
  e.clashes : /*empty*/ =
  e.cond (e.new-clashes) s.new?;

Check-Ft t.Ft (e.pos) (e.right-pos) t.name s.dir, t.Ft : {
  s.ObjectSymbol, {
    <?? t.name s.dir> : \{
      e (e.pos Sym) e = /*empty*/ Continue;
      e (e.pos (Ref e)) e = $fail;
    };
    s.dir : Left-checks,
      <?? t.name Right-checks> : \{
        e (e.right-pos Sym) e = /*empty*/ Continue;
        e (e.right-pos (Ref e)) e = $fail;
      };
    <Set-Var t.name (s.dir) (<?? t.name s.dir> (e.pos Sym))> = Sym Continue;
  };
  (PAREN e.expr), {
    <?? t.name s.dir> : \{
      e (e.pos (Ref e)) e = /*empty*/ Continue;
      e (e.pos Sym) e = $fail;
    };
    s.dir : Left-checks,
      <?? t.name Right-checks> : \{
        e (e.right-pos (Ref e)) e = /*empty*/ Continue;
        e (e.right-pos Sym) e = $fail;
      };
    s.dir : {
      Left-checks = "lderef";
      Right-checks = "rderef";
    } :: s.name-dir,
      t.name : (e.QualifiedName),
      <Gener-Label s.name-dir e.QualifiedName> :: t.ref-name,
//      <Declare-Vars "Expr" (VAR t.ref-name)> : e,
      <Set-Var t.name (s.dir) (<?? t.name s.dir> (e.pos (Ref t.ref-name)))> =
      Ref Continue;
  };
  (VAR t.Ft-name), {
    <Hard-Exp? t.Ft>, {
      <?? t.Ft-name Flat> : True, {
        <?? t.Ft-name Length> : 1, {
          <?? t.name s.dir> : \{
            e (e.pos Sym) e = /*empty*/ Continue;
            e (e.pos (Ref e)) e = $fail;
          };
          s.dir : Left-checks,
            <?? t.name Right-checks> : \{
              e (e.right-pos Sym) e = /*empty*/ Continue;
              e (e.right-pos (Ref e)) e = $fail;
            };
//          <?? t.Ft-name Instantiated> : True =
//            /*empty*/ Continue;
          <Set-Var t.name (s.dir) (<?? t.name s.dir> (e.pos Sym))> =
            Sym Continue;
        };
        <Set-Var t.name (s.dir) (<?? t.name s.dir> (e.pos Flat))> =
          Flat <Length-of t.Ft> Continue;
      };
      /*empty*/ Continue;
    };
    /*empty*/ Stop;
  };
};

Dereference-Subexpr e.clashes =
  e.clashes : e1 (e.t1 Dereference e.t2 (e.Re) (s.dir e.Pe)) e2 \?
  e.Re : (VAR t.name),
  <?? t.name Instantiated> : True,
//  <WriteLN Dereference!!! t.name <?? t.name Right-checks>>,
//  <Format e.Pe> : e.f1 t.Ft e.f2 \?
  e.Pe : e.f1 t.Ft e.f2 \?
  \{
    t.Ft : (PAREN e.expr),
      <Length-of e.f1> :: e.pos,
      {
        <?? t.name Left-checks> : e (e.pos (Ref t.ref-name)) e \!
          # \{ <?? t.ref-name Instantiated> : True; } =
          <Declare-Vars "Expr" (VAR t.ref-name)> : e,
          <Instantiate-Vars (VAR t.ref-name)>,
          (Assert (DEREF (VAR t.ref-name) e.Re (e.pos))) :: e.cond,
          (e.t1 Dereference e.t2 (e.Re) (s.dir e.Pe)) :: t.old-clash,
          {
            e.t1 e.t2 : e Without-object-symbols e = Without-object-symbols;
            /*empty*/;
          } :: e.wos,
          (<Gener-Label "clash"> &New-Clash-Tags e.wos
            ((VAR t.ref-name)) (s.dir e.expr)
          ) :: t.new-clash,
          s.dir : {
            LEFT =
              e.cond (e1 t.new-clash t.old-clash e2);
            RIGHT =
              e.cond (e1 t.old-clash t.new-clash e2);
          };
        t.Ft e.f2 : $r e.f3 (PAREN e.expr1) e.f4 \?
          1 <Length-of e.f4> :: e.pos,
          {
            <?? t.name Right-checks> : e (e.pos (Ref t.ref-name)) e \!
              # \{ <?? t.ref-name Instantiated> : True; } =
              <Declare-Vars "Expr" (VAR t.ref-name)> : e,
              <Instantiate-Vars (VAR t.ref-name)>,
              (Assert 
                (DEREF (VAR t.ref-name) e.Re (
                  (INFIX "-" (<Length-of e.Re>) (e.pos))
                ))
              ) :: e.cond,
              (e.t1 Dereference e.t2 (e.Re) (s.dir e.Pe)) :: t.old-clash,
              {
                e.t1 e.t2 : e Without-object-symbols e =
                  Without-object-symbols;
                /*empty*/;
              } :: e.wos,
              (<Gener-Label "clash"> &New-Clash-Tags e.wos
                ((VAR t.ref-name)) (s.dir e.expr1)
              ) :: t.new-clash,
              s.dir : {
                RIGHT =
                  e.cond (e1 t.new-clash t.old-clash e2);
                LEFT =
                  e.cond (e1 t.old-clash t.new-clash e2);
              };
            \!\!\! $fail;
          };
        \!\! $fail;
      };
    e.f2 : /*empty*/ =
      (e1 (e.t1 e.t2 (e.Re) (s.dir e.Pe)) e2);
  };

Compare-Subexpr e.clashes =
  e.clashes () () () Old $iter e.clashes : {
    (e.t1 Compare e.t2 (e.Re) (s.dir e.Pe)) e.rest,
      e.Re : (VAR t.name),
      <?? t.name Instantiated> : True =
      {
        e.t1 e.t2 : e Without-object-symbols e =
          /*empty*/ (e.t2) (e.Re) (e.Pe);
        <Get-Static-Exprs e.Re> :: e.Re (e.Re-decls),
          <Get-Static-Exprs e.Pe> :: e.Pe (e.Pe-decls) =
          e.Re-decls e.Pe-decls (e.t2 Without-object-symbols) (e.Re) (e.Pe);
      } :: e.new-asserts (e.t2) (e.Re) (e.Pe),
      e.Pe () () Continue $iter {
        e.format : t.Ft e.Fe,
          <Length-of e.left> :: e.pos,
          <Length-of t.Ft> :: e.len,
          <Length-of e.Fe> :: e.right-pos,
          {
            \{
              <?? t.name Left-compare> :
                e (t.Ft Left (0) (e.pos) e.len) e;
              <?? t.name Right-compare> :
                e (t.Ft Left (0) (e.right-pos) e.len) e;
            } =
               /*empty*/ Continue;
            <Compare-Ft t.Ft> : {
              /*empty*/ s.stop??? = /*empty*/ s.stop???;
              e.compare s.eq =
//                <WriteLN Compare e.compare s.eq>,
                t.Ft : (VAR t.Ft-name),
                <Set-Var t.name (Left-compare) (<?? t.name Left-compare>
                  (t.Ft Left (0) (e.pos) e.len))>,
                <Set-Var t.Ft-name (Left-compare)
                  (<?? t.Ft-name Left-compare>
                  (e.Re Left (e.pos) (0) e.len))>,
                e.compare : {
                  Empty = /*empty*/ Continue;
                  Instantiated =
                    (t.Ft) (0) (e.len) :: e.sub1,
                    (e.Re) (e.pos) (e.len) :: e.sub2,
                    { s.eq : EQ = 0; 1; } :: s.R,
                    (Used t.Ft e.Re)
                    (s.eq <Middle 0 s.R e.sub1> e.sub2) Continue;
//                    (s.eq ((FIRST t.Ft)) ((LAST t.Ft))
//                      ((FIRST e.Re) e.pos) ((FIRST e.Re) e.pos e.len)
//                    ) Continue;
                  (t.var s.dir1 (e.pos1) (0) e.len), s.dir1 : {
                    Left =
                      (t.var) (e.pos1) (e.len) :: e.sub1,
                      (e.Re) (e.pos) (e.len) :: e.sub2,
                      { s.eq : EQ = 0; 1; } :: s.R,
                      (Used t.var e.Re)
                      (s.eq <Middle 0 s.R e.sub1> e.sub2) Continue;
//                      (s.eq ((FIRST t.var) e.pos1)
//                        ((FIRST t.var) e.pos1 e.len)
//                        ((FIRST e.Re) e.pos)
//                        ((FIRST e.Re) e.pos e.len)
//                      ) Continue;
                    Right =
                      (t.var)
                      ((INFIX "-" ((LENGTH t.var)) (e.pos1) (e.len)))
                      (e.len) :: e.sub1,
                      (e.Re) (e.pos) (e.len) :: e.sub2,
                      { s.eq : EQ = 0; 1; } :: s.R,
                      (Used t.var e.Re)
                      (s.eq <Middle 0 s.R e.sub1> e.sub2) Continue;
//                      (s.eq
//                        ((INFIX "-"
//                          ((LAST t.var)) (e.pos1) (e.len))
//                        )
//                        ((INFIX "-" ((LAST t.var)) (e.pos1)))
//                        ((FIRST e.Re) e.pos)
//                        ((FIRST e.Re) e.pos e.len)
//                      ) Continue;
//                    <Set-Var t.name Left-compare
//                      <?? t.name Left-compare>
//                      (t.name1 s.dir (e.pos1) (e.pos) e.len)
                  };
                };
            };
          } :: e.Ft-cond s.stop? =
          e.Fe (e.left t.Ft) (e.new-cond e.Ft-cond) s.stop?;
      } :: e.format (e.left) (e.new-cond) s.stop?,
      \{
        e.format : /*empty*/ =
          e.rest (e.cond e.new-cond) (e.new-asserts)
          (e.new-clashes (e.t1 e.t2 (e.Re) (s.dir e.Pe))) New;
        s.stop? : Stop = e.format () (e.new-cond) Continue $iter {
          e.format : e.Fe t.Ft,
            <Length-of e.right> :: e.pos,
            <Length-of t.Ft> :: e.len,
            {
              <?? t.name Right-compare> : e (t.Ft Left (0) (e.pos) e.len) e =
                /*empty*/ Continue;
              <Compare-Ft t.Ft> : {
                /*empty*/ s.stop??? = /*empty*/ s.stop???;
                e.compare s.eq =
                  t.Ft : (VAR t.Ft-name),
                  <Set-Var t.name (Right-compare)
                    (<?? t.name Right-compare>
                    (t.Ft Left (0) (e.pos) e.len))>,
                  <Set-Var t.Ft-name (Left-compare)
                    (<?? t.Ft-name Left-compare>
                    (e.Re Right (e.pos) (0) e.len))>,
                  e.compare : {
                    Empty = /*empty*/ Continue;
                    Instantiated =
                      (t.Ft) (0) (e.len) :: e.sub1,
                      (e.Re)
                      ((INFIX "-" ((LENGTH e.Re)) (e.pos) (e.len)))
                      (e.len) :: e.sub2,
                      { s.eq : EQ = 0; 1; } :: s.R,
                      (Used t.Ft e.Re)
                      (s.eq <Middle 0 s.R e.sub1> e.sub2) Continue;
//                      (s.eq ((FIRST t.Ft)) ((LAST t.Ft))
//                        ((INFIX "-" ((LAST e.Re)) (e.pos) (e.len)))
//                        ((INFIX "-" ((LAST e.Re)) (e.pos)))
//                      ) Continue;
                    (t.var s.dir1 (e.pos1) (0) e.len), s.dir1 : {
                      Left =
                        (t.var) (e.pos1) (e.len) :: e.sub1,
                        (e.Re)
                        ((INFIX "-" 
                          ((LENGTH e.Re)) (e.pos) (e.len)
                        )) (e.len) :: e.sub2,
                        { s.eq : EQ = 0; 1; } :: s.R,
                        (Used t.var e.Re)
                        (s.eq <Middle 0 s.R e.sub1> e.sub2)
                        Continue;
//                        (s.eq ((FIRST t.var) e.pos1)
//                          ((FIRST t.var) e.pos1 e.len)
//                          ((INFIX "-"
//                            ((LAST e.Re)) (e.pos) (e.len)
//                          ))
//                          ((INFIX "-" ((LAST e.Re)) (e.pos)))
//                        ) Continue;
                      Right =
                        (t.var)
                        ((INFIX "-"
                          ((LENGTH t.var)) (e.pos1) (e.len)
                        )) (e.len) :: e.sub1,
                        (e.Re)
                        ((INFIX "-" 
                          ((LENGTH e.Re)) (e.pos) (e.len)
                        )) (e.len) :: e.sub2,
                        { s.eq : EQ = 0; 1; } :: s.R,
                        (Used t.var e.Re)
                        (s.eq <Middle 0 s.R e.sub1> e.sub2)
                        Continue;
//                        (s.eq
//                          ((INFIX "-"
//                            ((LAST t.var)) (e.pos1) (e.len)
//                          ))
//                          ((INFIX "-" ((LAST t.var)) (e.pos1)))
//                          ((INFIX "-"
//                            ((LAST e.Re)) (e.pos) (e.len)
//                          ))
//                          ((INFIX "-" ((LAST e.Re)) (e.pos)))
//                        ) Continue;
                    };
                  };
              };
            } :: e.Ft-cond s.stop? =
            e.Fe (t.Ft e.right) (e.new-cond e.Ft-cond) s.stop?;
        } :: e.format (e.right) (e.new-cond) s.stop?,
          s.stop? : Stop =
          e.rest (e.cond e.new-cond) (e.new-asserts)
          (e.new-clashes (e.t1 Compare e.t2 (e.Re) (s.dir e.Pe))) s.new?;
      };
    t.clash e.rest = e.rest (e.cond) (e.asserts) (e.new-clashes t.clash) s.new?;
  } :: e.clashes (e.cond) (e.asserts) (e.new-clashes) s.new?,
//  <WriteLN Compare-Subexpr e.clashes (e.cond) (e.asserts) (e.new-clashes) s.new?>,
  e.clashes : /*empty*/ =
  e.cond (e.asserts) (e.new-clashes) s.new?;

Compare-Ft {
  s.ObjectSymbol =
    <PrintLN "Compare-Ft: can't compare object symbols!">, $fail;
  (PAREN e.expr) =
    /*empty*/ Continue;
  (VAR t.name), {
    <Hard-Exp? (VAR t.name)>, {
      <?? t.name Instantiated> : True = Instantiated;
      <?? t.name Left-compare> : {
        t.compare e = t.compare;
        /*empty*/ = Empty;
      };
    } :: e.compare,
      {
        <?? t.name Flat> : True,
          <?? t.name Length> : 1 = FLAT-EQ;
        EQ;
      } :: s.eq =
      e.compare s.eq;
    /*empty*/ Stop;
  };
};

Get-Source e.clashes =
  e.clashes : e1 (e.tags (e.Re) (s.dir e.Pe)) e2,
  \{ 
    /*
     * If source is an instantiated variable then go to the next clash.
     */
    e.Re : (VAR t.name),
      <?? t.name Instantiated> : True = $fail;
    /*
     * If in source there is unknown variable then we can't compute it, so
     * go to the next clash.
     */
    e.Re $iter e.Re : {               
      (VAR t.name) e.rest =           
        \{                    
          <?? t.name Instantiated> : True;  
          <?? t.name Left-compare> : v;   
        }, e.rest;                
      t e.rest = e.rest;              
    } :: e.Re,                    
      e.Re : /*empty*/;             
  } =
//  <WriteLN Get-Source (e.tags (e.Re) (s.dir e.Pe))>,
  {
    e.Re : /*empty*/ =
      <Store-Vars (EVAR ("empty" 0))> : t.empty,
      <Set-Var ("empty") (Instantiated) (True)>,
      () () (e.tags (t.empty) (s.dir e.Pe));
    e.Re : (VAR t.name) =
      (e.Re) () (e.tags (e.Re) (s.dir e.Pe));
    {
      e.tags : e Without-object-symbols e =
        /*empty*/ (e.tags (e.Re) (s.dir e.Pe));
      <Get-Static-Exprs e.Re> :: e.Re (e.Re-decls),
        <Get-Static-Exprs e.Pe> :: e.Pe (e.Pe-decls) =
        e.Re-decls e.Pe-decls (e.tags Without-object-symbols (e.Re) (s.dir e.Pe));
    } :: e.asserts (e.tags (e.Re) (s.dir e.Pe)), {
      e.Re : (VAR t.name) =
        () (e.asserts) (e.tags (e.Re) (s.dir e.Pe));
      <Compose-Expr e.Re> :: e.compose (e.not-inst) s.flat?,
        <Gener-Label "compose"> :: t.name,
        <Declare-Vars "Expr" (VAR t.name)> :: e.decl,
        <Instantiate-Vars (VAR t.name)>,
        {
          s.flat? : 0 = <Set-Var t.name (Flat) (True)>;;
        },
        <Set-Var t.name (Length) (<Length-of e.Re>)>,
        <Set-Var t.name (Format) (<Format-Exp e.Re>)> =
        (e.not-inst) (e.asserts e.decl (ASSIGN (VAR t.name) e.compose))
        (e.tags ((VAR t.name)) (s.dir e.Pe));
    };
  } :: (e.not-inst) (e.decl) t.clash,
  (Assert <Get-Subexprs e.not-inst> e.decl) (e1 t.clash e2);

Compose-Expr e.Re =
  e.Re () () 0 $iter {
    e.Re : t.Rt e.rest, t.Rt : {
      s.ObjectSymbol =
        <PrintLN "Compose-Expr: can't deal with object symbols!">, $fail;
      (PAREN e.expr) =
        <Compose-Expr e.expr> :: e.expr (e.new-not-inst) s,
        (PAREN e.expr) (e.new-not-inst) 1;
      (VAR t.name) =
        {
          <?? t.name Instantiated> : True = /*empty*/;
          t.Rt;
        } :: e.new-not-inst,
        {
          <?? t.name Flat> : True = 0;
          1;
        } :: s.new-flat?,
        (Used t.Rt) t.Rt (e.new-not-inst) s.new-flat?;
    } :: e.new-compose (e.new-not-inst) s.new-flat? =
      e.rest (e.compose e.new-compose) (e.not-inst e.new-not-inst)
      <"+" s.flat? s.new-flat?>;
  } :: e.Re (e.compose) (e.not-inst) s.flat?,
  e.Re : /*empty*/ =
  e.compose (e.not-inst) s.flat?;

Comp-Cyclic e.clashes =
  e.clashes : e1 (e.t1 Unknown-length e.t2 (e.Re) (s.dir e.Pe)) e2 =
  e.Re : (VAR (e.QualifiedName)),
  <Split-Hard-Left e.Pe> :: e.left-hard,
  <Split-Hard-Right e.Pe> :: e.right-hard,
  e.Pe : e.left-hard e.Cycle e.right-hard,
  {
    e.left-hard e.right-hard : /*empty*/ = /*empty*/ (e.QualifiedName) ();
    <Gener-Label "ref" e.QualifiedName> :: t.name,
      t.name : (e.CycleName),
      <Declare-Vars "Expr" (VAR t.name)> : e,
      <Instantiate-Vars (VAR t.name)>,
      <Set-Var t.name (Format) (<Format-Exp e.Cycle>)>,
      (INFIX "-" (<Length-of e.Re>) (<Length-of e.right-hard>)) :: e.len,
      (Used e.Re)
      (SUBEXPR (VAR t.name) e.Re (<Length-of e.left-hard>) (e.len)) :: e.decl,
      <Set-Var t.name (Left-compare)
        ((e.Re Left (<Length-of e.left-hard>) (0) <Length-of (VAR t.name)>))>,
      <Set-Var (e.QualifiedName) (Left-compare) ((
        (VAR t.name) Left (0) (<Length-of e.left-hard>) <Length-of (VAR t.name)>
      ))> =
      (e.t1 Checked-length e.t2 (e.Re) (s.dir e.left-hard (VAR t.name) e.right-hard))
      (e.CycleName) (e.decl);
  } :: e.old-clash (e.CycleName) (e.decl),
  (VAR (e.CycleName)) :: t.var,
  <Gener-Label L "For" "Break"> :: t.break-label,
  <Gener-Label L "For" "Cont"> :: t.cont-label,
  s.dir : {
    LEFT =
      e.Cycle : t.var-e1 e.rest,
      t.var-e1 : (VAR (e.SplitName)),
      {
//        e.rest : t.var-e2 = t.var-e2;
        (VAR <Gener-Label "lsplit" e.CycleName>);
      } :: t.var-e2,
      <Declare-Vars "Expr" t.var-e2> : e,
      <Instantiate-Vars t.var-e1 t.var-e2>
      (Assert 
        e.decl
        (LSPLIT t.var ((VAR ("min" e.SplitName))) t.var-e1 t.var-e2)
      )
      (Cond LABEL t.break-label)
      (Cond FOR (t.cont-label) () ((INC-ITER t.var)))
      (Fail (BREAK t.break-label))
      (Clear-Restricted)
      (<Update-Ties t.var-e2 <Update-Ties t.var-e1 e1>>
        e.old-clash
        (<Gener-Label "clash"> &New-Clash-Tags (t.var-e2) (s.dir e.rest))
      <Update-Ties t.var-e2 <Update-Ties t.var-e1 e2>>)
      ((CONTINUE t.cont-label));
    RIGHT =
      e.Cycle : e.rest t.var-e2,
      t.var-e2 : (VAR (e.SplitName)),
      {
//        e.rest : t.var-e2 = t.var-e2;
        (VAR <Gener-Label "lsplit" e.CycleName>);
      } :: t.var-e1,
      <Declare-Vars "Expr" t.var-e1> : e,
      <Instantiate-Vars t.var-e1 t.var-e2>
      (Assert 
        e.decl
        (RSPLIT t.var ((VAR ("min" e.SplitName))) t.var-e1 t.var-e2)
      )
      (Cond LABEL t.break-label)
      (Cond FOR (t.cont-label) () ((INC-ITER t.var)))
      (Fail (BREAK t.break-label))
      (Clear-Restricted)
      (<Update-Ties t.var-e2 <Update-Ties t.var-e1 e1>>
        e.old-clash
        (<Gener-Label "clash"> &New-Clash-Tags (t.var-e1) (s.dir e.rest))
      <Update-Ties t.var-e2 <Update-Ties t.var-e1 e2>>)
      ((CONTINUE t.cont-label));
  };

Get-Subexprs e.vars =
//  <WriteLN Get-Subexprs e.vars>,
  e.vars () $iter {
    e.vars : (VAR t.name) e.rest,
      # \{ <?? t.name Instantiated> : True; },
      <?? t.name Left-compare> : (t.var s.dir (e.pos) (0) e.len) e =
      <Instantiate-Vars (VAR t.name)>,
      <Declare-Vars "Expr" (VAR t.name)> : e,
      {
        s.dir : Right =
          (INFIX "-" (<Length-of t.var>) (e.pos e.len));
        e.pos;
      } :: e.pos,
      e.rest (e.decls (Used t.var) (SUBEXPR (VAR t.name) t.var (e.pos) (e.len)));
    // STUB:
    e.vars : t e.rest = e.rest (e.decls);
  } :: e.vars (e.decls),
  e.vars : /*empty*/ =
  e.decls;

/*
 * Returns those parts of e.expr which lengthes are known. Also returns a list
 * of variables with unknown lengthes.
 */
Unknown-Vars e.expr =
  e.expr () () $iter {
    e.expr : t.first e.rest, {
      t.first : (VAR t.name), {
        <?? t.name Instantiated> : True =
          e.new-expr t.first (e.unknown);
        <?? t.name Max> :: e.max, <?? t.name Min> : e.max =
          e.new-expr t.first (e.unknown);
        e.new-expr (e.unknown t.first);
      };
      e.new-expr t.first (e.unknown);
    } :: e.new-expr (e.unknown) =
      e.rest (e.new-expr) (e.unknown);
  } :: e.expr (e.new-expr) (e.unknown),
  e.expr : /*empty*/ =
  e.new-expr (e.unknown);
  
Split-Hard-Left e.expr =
  e.expr () $iter {
    e.expr : t.Pt e.rest, {
      <Hard-Exp? t.Pt> = e.rest (e.hard t.Pt);
      (e.hard);
    };
  } :: e.expr (e.hard),
  e.expr : /*empty*/ =
  e.hard;

Split-Hard-Right e.expr =
  e.expr () $iter {
    e.expr : e.some t.Pt, {
      <Hard-Exp? t.Pt> = e.some (t.Pt e.hard);
      (e.hard);
    };
  } :: e.expr (e.hard),
  e.expr : /*empty*/ =
  e.hard;

Gener-Label e.QualifiedName =
  {
    <Lookup &Labels e.QualifiedName> : s.num,
      <"+" s.num 1>;
    1;
  } :: s.num,
  <Bind &Labels (e.QualifiedName) (s.num)>,
  (e.QualifiedName s.num);

Comp-Re e.Re (e.Snt) =
//  <WriteLN Re e.Re>,
  \{
    e.Snt : e.rest-Snt (Comp Sentence) e.other-Snts \?
      {
        /*
         * e.Re is NOT the last if in the e.Snt there is any term which
         * differs form (Comp e) or we are inside a negation.
         */
        e.rest-Snt : e t.item e,
          # \{ 
            t.item : (Comp e);
          } \! $fail;
        e.Snt : \{
          e (Comp Not) e;
          e (Comp Error) e;
          e (Comp Notail) e; // ?????????????
        } \! $fail;
        /*
         * If we can reach here then our Re is the last action in the
         * current path. So we should do TAILCALL or simply assign
         * values to the function output variables. We can get $fail in
         * the following block only in the case of an error. So we send
         * this $fail to the upper sentence.
         */
        {
          e.Re : (CALL t.Fname e.arg-Re) \?
            {
              <In-Table? &Fun? t.Fname> \? \{
                /*
                 * If the sentence doesn't end with 
                 * (Comp Retfail) then we can't do tailcall.
                 */
                # \{ e.Snt : e (Comp Retfail); } \!\! $fail;
                /*
                 * Else, if there was '=' after all '\!' and we
                 * are not inside a source block then CAN do
                 * tailcall.
                 */
                e.other-Snts : (Comp Cutall) e.rest,
                  # \{ e.rest : e (Comp Notail) e; } \! $fail;
                /* Else, we CAN do tailcall if we are on the
                 * last branch and there weren't any cuts or
                 * NOFAIL blocks.
                 */
                e.other-Snts : e t.item1 e, \{ 
                  # t.item1 : \{ 
                    (Comp s);
                  } \!\! $fail;
                  t.item1 : \{
                    (Comp Cut);
                    (Comp Source (Nofail));
                  } \!\! $fail;
                };
              };
              \!
              # \{ e.rest-Snt : e (Comp Trap) e; },
                <Lookup-Func t.Fname> :: s s.tag t (e.Fin) (e.Fout),
                <Split-Re (<? &Out-Format>) e.Fout> :: e.out,
                <Split &Second-Empty? (<Zip (<? &Res-Vars>) (e.out)>)>
                  :: (e.empty) (e.res-vars),
                <Map &Good-Res-Var? (e.res-vars)> : e =
                <Comp-Calls e.arg-Re> :: e.calls,
                <Get-Static-Exprs <? &Last-Re>> :: e.comp-Re (e.decls),
                <Split-Re (e.Fin) e.comp-Re> :: e.sp-Re,
                (e.calls) e.decls
                <Comp-Assigns (<Map &Get-Elem 0 (e.empty)>)
                  <Map &Get-Elem 1 (e.empty)>>
                (Used <Vars e.arg-Re>)
                (TAILCALL t.Fname (e.sp-Re)
                  (<Map &Get-Elem 0 (e.res-vars)>));
            };
          <Comp-Calls e.Re> :: e.calls,
            <Get-Static-Exprs <? &Last-Re>> :: e.comp-Re (e.decls),
            <Split-Re (<? &Out-Format>) e.comp-Re> :: e.splited-Re,
            (e.calls)
            e.decls <Comp-Assigns (<? &Res-Vars>) e.splited-Re> RETURN;
        };
      };
    <Comp-Calls e.Re> :: e.calls,
//      <WriteLN! &StdErr "Re Snt" e.Snt>,
      (e.calls)
      <Comp-Sentence () e.Snt>;
  } :: (e.calls) e.asail-Snt,
//  <WriteLN! &StdErr "Re asail-Snt" e.asail-Snt>,
//  <WriteLN! &StdErr "Re calls" e.calls>,
  \{
    e.calls : e (Roll-back t) e =
      e.Snt : e.Current-Snt (Comp Sentence) e.Other-Snts =
//      <Comp-Sentence () e.Other-Snts> :: e.asail-Others,
      e.asail-Snt (e.calls) $iter {
        e.calls : {
          e.first-calls (Roll-back t.call) =
            (IF (t.call) e.asail-Snt) (e.first-calls);
          e.first-calls t.call, {
//            t.call : (CALL t.Fname t.args (e.ress)),
//              <In-Table? &Without-Sideffects t.Fname> =
//              (If-used (e.ress) t.call);
            t.call;
          } :: t.call =
            t.call e.asail-Snt (e.first-calls);
        };
      } :: e.asail-Snt (e.calls),
      e.calls : /*empty*/ =
      e.asail-Snt // e.asail-Others;
      <Comp-Sentence () e.Other-Snts>;
    e.calls e.asail-Snt;
  };

Second-Empty? (t.var ()) = ;

Good-Res-Var? (t.var (t.F-var)) = ;

Comp-Calls e.Re =
//  <WriteLN Calls e.Re>,
  e.Re () () $iter e.Re : {
    (CALL t.Fname e.arg-Re) e.rest-Re =
      <Lookup-Func t.Fname> :: s s.tag t (e.Fin) (e.Fout),
      (Used <Vars e.arg-Re>) :: e.used,
      <Comp-Calls e.arg-Re> :: e.arg-calls,
      <Split-Re (e.Fin) <? &Last-Re>> :: e.splited-Re,
//      <WriteLN Comp-Calls e.splited-Re>,
      <Get-Static-Exprs e.splited-Re> :: e.splited-Re (e.decls),
      t.Fname : (e.QualifiedName),
      e.QualifiedName "res" :: e.prefix,
      /*
       * We want to generate variables with the names
       * (e.QualifiedName "res" s.num).
       * Find maximum s.num used with such prefix.
       */
      0 <Domain &Vars-Tab> $iter {
        e.vars : e1 ((e.prefix s.n)) e2 =
          <Max s.n s.num> : s.max,
          s.max e2;
        s.num;
      } :: s.num e.vars,
      e.vars : /*empty*/ =
      <Del-Pragmas <Gener-Vars s.num (e.Fout) e.prefix>> : e.res-Re s,
      <Store-Vars <Vars e.res-Re>> :: e.ress,
      <Instantiate-Vars e.ress>,
      <Ref-To-Var <Strip-STVE e.res-Re>> :: e.res-Re,
      e.decls <Declare-Vars "Expr" e.ress> :: e.decls,
      {
        s.tag : FUNC? =
          (Roll-back (CALL t.Fname (e.splited-Re) (e.ress)));
        (CALL t.Fname (e.splited-Re) (e.ress));
      } :: t.call,
      e.rest-Re 
      (e.calls e.arg-calls e.decls e.used t.call)
      (e.comp-Re e.res-Re);
    (PAREN e.paren-Re) e.rest-Re =
      <Comp-Calls e.paren-Re> :: e.paren-calls,
      <? &Last-Re> :: e.comp-paren-Re,
      e.rest-Re (e.calls e.paren-calls) (e.comp-Re (PAREN e.comp-paren-Re));
//    (REF e) e.rest-Re =
//      e.rest-Re (e.calls) (e.comp-Re);
    t.Rt e.rest-Re =
      e.rest-Re (e.calls) (e.comp-Re t.Rt);
  } :: e.Re (e.calls) (e.comp-Re),
  e.Re : /*empty*/,
  <Store &Last-Re e.comp-Re>,
  e.calls;

/*
 * For the future...
 */
//Norm-Vars e.Sentence =
//  e.Sentence () $iter {
//    e.Sentence : t.Statement e.rest, {
//      t.Statement : \{
//        (SVAR e.var) = "s" e.var;
//        (TVAR e.var) = "v" e.var;
//        (EVAR e.var) = "e" e.var;
//        (VVAR e.var) = "t" e.var;
//      } : s.var-sym e.NEW (e.QualifiedName),
//        {
//          e.NEW : NEW = (e.QualifiedName);
//          (s.var-sym e.QualifiedName);
//        } :: t.name,

Store-Vars e.vars =
//  <WriteLN Store-Vars e.vars>,
  e.vars () $iter {
    e.vars : (s.var-tag (e.QualifiedName s.last)) e.rest,
      {
        s.last : 0 = (e.QualifiedName);
        <Int? s.last> = (e.QualifiedName s.last);
        /*empty*/ =
          s.var-tag : {
            SVAR = "s";
            TVAR = "t";
            VVAR = "v";
            EVAR = "e";
            VAR = /*empty*/;
          } :: e.var-sym,
          (e.var-sym e.QualifiedName s.last);
      } :: t.name,
      {
        <In-Table? &Vars-Tab t.name>; // do nothing
        <Table> :: s.tab, <Bind &Vars-Tab (t.name) (s.tab)>,
          {
            s.var-tag : VAR =
              <Lookup &Var-Tags (VAR t.name)>;
            s.var-tag;
          } : {
            SVAR =
              <Set-Var t.name (Min) (1)>,
              <Set-Var t.name (Max) (1)>,
              <Set-Var t.name (Length) (1)>,
              <Set-Var t.name (Flat) (True)>;
            TVAR =
              <Set-Var t.name (Min) (1)>,
              <Set-Var t.name (Max) (1)>,
              <Set-Var t.name (Length) (1)>;
            VVAR =
              <Set-Var t.name (Min) (1)>;
//              <Set-Var t.name (Max) ()>;
            EVAR =
              <Set-Var t.name (Min) (0)>;
//              <Set-Var t.name (Max) ()>;
          },
          <Set-Var t.name (Left-compare) ()>,
          <Set-Var t.name (Right-compare) ()>,
          <Set-Var t.name (Left-checks) ()>,
          <Set-Var t.name (Right-checks) ()>,
          <Set-Var t.name (Format) ((VAR t.name))>;
      },
      e.rest (e.new-vars (VAR t.name));
  } :: e.vars (e.new-vars),
  e.vars : /*empty*/ =
  e.new-vars;

Declare-Vars s.type e.vars =
  e.vars () $iter {
    e.vars : (VAR t.name) e.rest, {
      <?? t.name Declared> : True;  // do nothing
      {
        <In-Table? &Vars-Tab t.name>; // do nothing
        <Table> :: s.tab, <Bind &Vars-Tab (t.name) (s.tab)>,
          <Set-Var t.name (Left-compare) ()>,
          <Set-Var t.name (Right-compare) ()>,
          <Set-Var t.name (Left-checks) ()>,
          <Set-Var t.name (Right-checks) ()>,
          <Set-Var t.name (Format) ((VAR t.name))>,
          <Set-Var t.name (Min) (0)>;
      },
        <Set-Var t.name (Declared) (True)>,
        (DECL s.type (VAR t.name));
    } :: e.new-decl,
    e.rest (e.decls e.new-decl);
  } :: e.vars (e.decls),
  e.vars : /*empty*/ =
  e.decls;

Instantiate-Vars e.vars =
  e.vars $iter {
    e.vars : (VAR t.name) e.rest,
      <Set-Var t.name (Instantiated) (True)>,
      e.rest;
  } :: e.vars,
  e.vars : /*empty*/;

Comp-Assigns (e.vars) e.splited-Re =
//  <WriteLN Comp-Assigns '<'e.vars'>' e.splited-Re>,
  <Instantiate-Vars e.vars>,
  e.vars (e.splited-Re) () $iter {
    e.vars : t.var e.rest-vars, 
      e.splited-Re : (e.Re) e.rest-Re,
      t.var : (VAR t.name),
      <Set-Var t.name (Format) (<Format-Exp e.Re>)>,
      <Get-Static-Exprs e.Re> :: e.Re (e.decls),
      e.rest-vars (e.rest-Re)
      (e.assignments e.decls
        (If-used (t.var) (Used <Vars e.Re>) (ASSIGN t.var e.Re))
      );
  } :: e.vars (e.splited-Re) (e.assignments),
  e.vars : /*empty*/,
  e.assignments;

Get-Static-Exprs e.Re =
  e.Re () () () $iter {
    e.Re : t.Rt e.rest, t.Rt : {
      s.ObjectSymbol, {
        <Char? t.Rt> =
          e.rest (e.new-Re) (e.decls) (e.expr t.Rt);
        <Get-Static-Var "chars" e.expr> :: e.expr-var (e.expr-decl),
          {
            <Int? t.Rt> = "int";
            <Word? t.Rt> = "word";
          } :: s.prefix,
          <Get-Static-Var s.prefix t.Rt> :: e.Rt-var (e.Rt-decl) =
          e.rest (e.new-Re e.expr-var e.Rt-var)
          (e.decls e.expr-decl e.Rt-decl) ();
      };
      (PAREN e.paren-Re) =
        <Get-Static-Exprs e.paren-Re> :: e.new-paren-Re (e.paren-decls),
        <Get-Static-Var "chars" e.expr> :: e.expr-var (e.expr-decl),
        e.rest (e.new-Re e.expr-var (PAREN e.new-paren-Re))
        (e.decls e.expr-decl e.paren-decls) ();
      t.var =
        <Get-Static-Var "chars" e.expr> :: e.expr-var (e.expr-decl),
        e.rest (e.new-Re e.expr-var t.var) (e.decls e.expr-decl) ();
    };
  } :: e.Re (e.new-Re) (e.decls) (e.expr),
//  <WriteLN Get-Static-Exprs e.Re>,
  e.Re : /*empty*/ =
  <Get-Static-Var "chars" e.expr> :: e.expr-var (e.expr-decl),
  e.new-Re e.expr-var (e.decls e.expr-decl);

Get-Static-Var s.prefix e.expr, {
  e.expr : /*empty*/ = /*empty*/ ();
  {
    <Lookup &Static-Exprs s.prefix e.expr> : t.var = t.var ();
    ("const" s.prefix e.expr) :: t.name,
      <Bind &Static-Exprs (s.prefix e.expr) ((VAR t.name))>,
      <Declare-Vars "Expr" (VAR t.name)> : e,
      <Instantiate-Vars (VAR t.name)>,
      <Set-Var t.name (Flat) (True)>,
      <Length e.expr> :: s.len,
      <Set-Var t.name (Length) (s.len)>,
      <Set-Var t.name (Min) (s.len)>,
      <Set-Var t.name (Max) (s.len)>,
      <Set-Var t.name (Format) (e.expr)> =
      (VAR t.name) ((EXPR (VAR t.name) e.expr));
  };
};

/*
 * Generates indexes for all varibles in e.Format and returns e.Format with all
 * (?VAR) changed to (?VAR (e.Name)) and s.max. e.Name is all words from
 * e.prefix plus unical number. Numbers are generated sequentially starting
 * with s.num. s.max is the maximum of all generated numbers.
 */
Gener-Vars s.num (e.Format) e.prefix, {
  e.Format : t.Ft e.rest, t.Ft : {
    s.ObjectSymbol = t.Ft <Gener-Vars s.num (e.rest) e.prefix>;
    (REF e) = t.Ft <Gener-Vars s.num (e.rest) e.prefix>;
    (PAREN e.Fe) =
      <Gener-Vars s.num (e.Fe) e.prefix> :: expr s.num,
      (PAREN expr) <Gener-Vars s.num (e.rest) e.prefix>;
    (s.VariableTag) =
      <"+" s.num 1> :: s.num,
      (s.VariableTag (PRAGMA) (e.prefix s.num)) <Gener-Vars s.num (e.rest) e.prefix>;
  };
  /*
   * e.Format is empty, so return s.num -- the last term in the answer.
   */
  s.num;
};

Strip-STVE expr = <Subst (SVAR TVAR VVAR EVAR) ((VAR) (VAR) (VAR) (VAR)) expr>;

Vars e.expr =
  e.expr () $iter {
    e.expr : t.first e.rest,
      t.first : {
        s.ObjectSymbol = /*empty*/;
        (REF t.Name) = /*empty*/; 
        (PAREN e.ResultExpression) = <Vars e.ResultExpression>;
        (CALL (PRAGMA (e) e) t.Fname e.ResultExpression) =
          <Vars e.ResultExpression>;
        (CALL t.Fname e.ResultExpression) = <Vars e.ResultExpression>;
        /*
         * Next line is needed for obtaining a list of known variables
         * from &Var-Stack. Function Vars is never called for abstract
         * syntax's block.
         */
//        (BLOCK e.vars1) = <Vars e.vars1>;
        t.var = t.var;  // t.var ::= (EVAR t.Name) | (VVAR t.Name)
                //      | (TVAR t.Name) | (SVAR t.Name)
      } :: e.var =
      e.rest (e.vars e.var);
  } :: e.expr (e.vars),
  e.expr : /*empty*/ =
  e.vars;

Length-of {
  /*empty*/ = 0;
  e.Re =
    e.Re () $iter {
      e.Re : t.Rt e.rest, t.Rt : {
        s.ObjectSymbol = 1;
        (PAREN e) = 1;
        (REF t.name) = <Ref-Len t.name>;
        (VAR t.name), {
          <?? t.name Length>;
          (Used t.Rt) (LENGTH t.Rt);
        };
      } :: e.new-len,
      e.rest (e.Length e.new-len);
    } :: e.Re (e.Length),
    e.Re : /*empty*/ =
//    (INFIX "+" e.Length);
//    <WriteLN Length e.Length>,
    e.Length;
};

Ref-Len t.name = {
  <To-Int <Lookup &Const-Len t.name>>;
  <Length <Length-of <Lookup &Const t.name>>> :: s.len =
    <Bind &Const-Len (t.name) (s.len)>,
    s.len;
};

/*
 * Ends good if lengths of all variables in e.expr can be calculated.
 */
Hard-Exp? e.expr =
  e.expr $iter {
    e.expr : t.first e.rest =
    {
      t.first : (VAR t.name), {
        <?? t.name Instantiated> : True;
        <?? t.name Max> :: e.max, <?? t.name Min> : e.max;
        = $fail;
      };;
    },
      e.rest;
  } :: e.expr,
  e.expr : /*empty*/;

Parenthesize-Operators e.Snt = <Map &Paren-Op (e.Snt)>;

Paren-Op t.Op, {
  t.Op : (s.tag e),
    RESULT LEFT RIGHT HARD : e s.tag e = t.Op;
  NOFAIL FAIL CUTALL CUT STAKE ERROR : e t.Op e = (t.Op);
  t.Op : (e.expr) = (<Parenthesize-Operators e.expr>);
  t.Op;
};

///*
// * Add "VAR" before each SVAR, TVAR, VVAR, and EVAR.
// */
//Norm-Vars e.Snt =
//  () e.Snt $iter {
//    e.Snt : t.Statement e.rest, {
//      t.Statement : \{ (SVAR e); (TVAR e); (VVAR e); (EVAR e); } =
//        t.Statement : (e.var),
//        (e.new-Snt (VAR e.var)) e.rest;
//      t.Statement : (e.expr) =
//        (e.new-Snt (<Norm-Vars e.expr>)) e.rest;
//      /*
//       * Else we have symbol. So proceed with the rest.
//       */
//      (e.new-Snt t.Statement) e.rest;
//    };
//  } :: (e.new-Snt) e.Snt,
//  e.Snt : /*empty*/ =
//  e.new-Snt;
  
Print-Error s.WE e.Descrip t.Pragma =
  <? &Error-Counter> : s.n,
  <Store &Error-Counter <"+" s.n 1>>,
  <Print-Pragma &StdErr t.Pragma>,
  <Print! &StdErr " " s.WE " ">,
  s.WE e.Descrip : {
    Error! Re = <PrintLN! &StdErr "Wrong format of result expression">;
    Error! Call = <PrintLN! &StdErr "Wrong argument format in function call">;
    Error! Pattern = <PrintLN! &StdErr "Wrong format of pattern expression">;
    Warning! Pattern = <PrintLN! &StdErr "Clash can't be solved">;
    Error! Var-Re t.var =
      <PrintLN! &StdErr "Unknown variable '"
                <AS-To-Ref t.var> "' in result expression">;
    Error! Var-Hard t.var =
      <PrintLN! &StdErr "Repeated occurence of the variable '"
                <AS-To-Ref t.var> "' in hard expression">;
    Error! Var-Type t.var s.type =
      <PrintLN! &StdErr "Incorrect type '" <AS-To-Ref s.type>
                "' of the variable '" <AS-To-Ref t.var> "'">;
    Error! Cut = <PrintLN! &StdErr "'\\\\!' without corresponding '\\\\?'">;
  };

Print-Pragma s.channel (PRAGMA e.pragmas),
  e.pragmas : {
    e (FILE e.file-name) e, <Print! s.channel e.file-name>, $fail;
    e (LINE s.line s.col) e, <Print! s.channel (s.line ", " s.col)>, $fail;
    e = <Print! s.channel ":">;
  };

AS-To-Ref {
  SVAR = 's';
  TVAR = 't';
  VVAR = 'v';
  EVAR = 'e';
  (s.tag t (e.name)) = <AS-To-Ref s.tag> '.' <To-Chars e.name>;
};

?? t.name e.key =
  <Lookup &Vars-Tab t.name> : s.tab,
  <Lookup s.tab e.key>;

Set-Var t.name (e.key) (e.val) =
//  <WriteLN Set-Var t.name (e.key)>,
  <Lookup &Vars-Tab t.name> : s.tab,
  <Bind s.tab (e.key) (e.val)>;

Lookup-Func t.Fname, \{
  <Lookup &Fun t.Fname>;
  <Lookup &Fun? t.Fname>;
} : s.linkage s.tag t.pragma (e.Fin) (e.Fout) =
  s.linkage s.tag t.pragma (e.Fin) (e.Fout);