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

$use Access Box Compare StdIO Table;

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

// verifies that all constructions in e.Sentence have right formats
$func? Satisfies-Format? (e.InFormat) (e.OutFormat) e.Sentence = ;

// verifies that all function calls found in e.expr have appropriate input
// formats
$func Check-Inputs e.Sentence = ;

// verifies that all vars in e.Sentence are defined for the moment of use and
// that there aren't repeated indexes in hard expressions
$func Check-Vars (e.vars) e.Sentence = ;

// for each new var verifies that it is realy new (then adds it to the var
// list) or that it has right type
$func Update-Vars s.format (e.vars) e.new-vars = e.updated-vars;

// returns the maximum (by length) sequence of cuts contained in the argument
$func? Get-Cuts t.Branch-or-Block = e.cuts-sequence;


RFP-Check e.Items, {
  e.Items : e t.item e,
    {
      <Lookup &RFP-Options ITEMS> : v.targets =
        v.targets : e t.name e,
        t.item : (t t t t.name e);;
    },
    t.item : (s.linkage s.tag t.pragma t.name (e.in) (e.out) t.branch),
    s.tag : \{ FUNC; FUNC?; },
    { <Satisfies-Format? (<Format-Exp e.in>) (<Format-Exp e.out>) t.branch>;; },
    <Check-Vars (<Vars e.in>) t.branch>,
    { <Print-Error Error! Cut <R 0 <Get-Cuts t.branch>>>;; },
    $fail;;
};

/*
 *  Verifies that:
 * 1) Result of e.Sentence computing has format not wider than e.OutFormat.
 * 2) All constructions in e.Sentence returns expressions of right formats.
 * 3) e.Sentence deals with expressions with format under e.InFormat only.
 * 4) All function calls are performed with expressions of right formats.
 */
Satisfies-Format? (e.InFormat) (e.OutFormat) e.Sentence =
  e.Sentence (e.OutFormat) $iter {
    e.Sentence : $r e.Snt (ERROR t) e.queue =
      <Satisfies-Format? () ((EVAR)) e.queue>,
      e.Snt ();
    e.Sentence : e.Snt t.Statement,
      t.Statement : {
        (RESULT t.Pragma e.ResultExpression) =
          {
            <Subformat? (e.OutFormat) (<Format-Exp e.ResultExpression>)> =
              <Check-Inputs e.ResultExpression>,
              e.Snt ();
            <Print-Error Error! Re t.Pragma> = $fail;
              /*
               * So in the case of an error we can only return
               * coordinates of the whole result expression, but
               * not the concrete position of the error in a
               * block if the later has place.
               */
          };
        (FORMAT t.Pragma e.HardExpression) =
//          \{
//            <Subformat? (e.OutFormat) ()> =
              e.Snt (<Format-Exp e.HardExpression>);
//            <Print-Error Error! Re t.Statement>, $fail;
//          };
        (s.block t e.Branches), s.block : \{ BLOCK; BLOCK?; } =
          {
            e.Snt : /*empty*/ = /*empty*/;
            (Comp Branch);
          } :: e.pref,
          {
            e.Branches : e (BRANCH t e.Snt1) e,
              <Satisfies-Format? (e.InFormat) (e.OutFormat) e.pref e.Snt1>,
              $fail;
            e.Snt ((EVAR));
          };
        (NOT (BRANCH t e.Snt1)) =
          \{
            <Subformat? (e.OutFormat) ()>,
              e.Snt e.Snt1 ();
            <Print-Error Error! Re t.Statement>, $fail;
          };
        (ITER (BRANCH t e.Snt1) (FORMAT t.Pragma e.HardExp) (BRANCH t e.Snt2)) =
          <Format-Exp e.HardExp> :: e.HardFormat,
          <Satisfies-Format? () (e.HardFormat) e.Snt1>,
          e.Snt (FORMAT t.Pragma e.HardExp) e.Snt2 (e.OutFormat);
        (TRY (BRANCH t e.Snt1) e.NOFAIL t.CatchBlock) = 
          <Satisfies-Format? () (e.OutFormat) e.Snt1>,
          <Satisfies-Format? ((EVAR)) (e.OutFormat) t.CatchBlock>,
          e.Snt ();
        (s.tag t.Pragma e.PatternExpression), s.tag : \{ LEFT; RIGHT; } =
//          {
//            <Subformat? (e.OutFormat) ()>,
              {
                e.Snt : /*empty*/ =
                  <Format-Exp e.PatternExpression> :: e.PatternFormat,
                  {
                    <Subformat? (e.InFormat) (e.PatternFormat)> =
                      /*empty*/ ();
                    <Print-Error Error! Pattern t.Pragma> = $fail;
                  };
                e.Snt ((EVAR));
              };
//            <Print-Error Error! Re t.Statement> \! $fail;
//          };
        NOFAIL = e.Snt ();
        (FAIL t) = e.Snt ();
        (CUTALL t) = e.Snt ();
        (CUT t) = e.Snt ();
        (STAKE t) = e.Snt ();
        (BRANCH t e.Snt1) = e.Snt1 (e.OutFormat);
        (Comp Branch) = /*empty*/ ();
      };
  } :: e.Sentence (e.OutFormat),
  e.Sentence : /*empty*/;

/*
 * Verifies that all function calls found in e.expr have appropriate input
 * formats.
 */
Check-Inputs {
  t.first e.rest, t.first : {
    (CALL t.Pragma t.Fname e.ResultExpression), {
      <L 3 <Lookup-Func t.Fname>> : (e.Fin),
        # <Subformat? (e.Fin) (<Format-Exp e.ResultExpression>)> =
        <Print-Error Error! Call t.Pragma>;;
    },
      <Check-Inputs e.ResultExpression>;
    (PAREN e.paren-expr) = <Check-Inputs e.paren-expr>;
    t.var-or-symbol = /*empty*/;
  },
    <Check-Inputs e.rest>;
  /*empty*/ = /*empty*/;
};

/*
 * Verifies that all vars in e.Sentence are defined for the moment of use and
 * that there are not repeated indexes in hard expressions.
 * e.vars are known variables for the moment we have e.Sentence to dial with.
 */
Check-Vars (e.vars) e.Sentence =
  (e.vars) e.Sentence $iter \{
    e.Sentence : t.Statement e.Snt,
      t.Statement : {
        (RESULT t e.Re) =
          {
            <Vars e.Re> : e (s.type t.Pragma e.name) e,
              {
                e.vars : e (s.t t.p e.name) e,
                  {
                    s.t : s.type;
                    <Print-Error Error!
                      Var-Type (s.t t.p e.name) s.type t.Pragma>;
                  };
                <Print-Error Error!
                  Var-Re (s.type t.Pragma e.name) t.Pragma>;
              },
              $fail;
            e.vars;
          };
        (FORMAT t e.He) =
          <Vars e.He> : e.He-vars,
          {
            \? e.He-vars : e (s1 t.p1 e3) e (s2 t.p2 e3) e4,
              {
                s1 : s2;
                <Print-Error Error! Var-Type (s1 t.p1 e3) s2 t.p2>;
              },
              <Print-Error Error! Var-Hard (s1 t.p1 e3) t.p2>,
              e4 : /*empty*/ \! $fail;
            <Update-Vars Format (e.vars) <Reverse e.He-vars>>;
          };
        (LEFT  t e.Pe) = <Update-Vars Pattern (e.vars) <Vars e.Pe>>;
        (RIGHT t e.Pe) = <Update-Vars Pattern (e.vars) <Vars e.Pe>>;
        (s.block t e.Branches), s.block : \{ BLOCK; BLOCK?; } =
          {
            e.Branches : e t.branch e,
              <Check-Vars (e.vars) t.branch>,
              $fail;
            e.vars;
          };
        (BRANCH t e.Snt1) =
          <Check-Vars (e.vars) e.Snt1>,
          e.vars;
        (ITER t.IterBody t.IterVars t.IterCondition) =
          <Check-Vars (e.vars) t.IterVars t.IterBody>,
          t.IterVars : (FORMAT t e.He),
          <Update-Vars Format (e.vars) <Vars e.He>> :: e.vars,
          <Check-Vars (e.vars) t.IterCondition>,
          e.vars;
        (TRY t.TryBranch e.NOFAIL t.CatchBlock) =
          <Check-Vars (e.vars) t.TryBranch>,
          <Check-Vars (e.vars) t.CatchBlock>,
          e.vars;
        t.any-other = e.vars;
      } :: e.vars,
      (e.vars) e.Snt;
  } :: (e.vars) e.Sentence,
  e.Sentence : /*empty*/;

/*
 * For each new var verifies that it is realy new (then adds it to the var
 * list) or that it has right type. Returns updated list of variables.
 */
Update-Vars s.format? (e.vars) e.new-vars =
  (e.vars) e.new-vars $iter {
    e.new-vars : (s.type t.p2 e.name) e.rest,
      e.vars : {
        e (s.type t e.name) e = (e.vars) e.rest;
        e1 (s.t t.p1 e.name) e2, {
          s.format? : Format =
            (e1 e2 (s.type t.p2 e.name)) e.rest;
          <Print-Error Error! Var-Type (s.t t.p1 e.name) s.type t.p2>,
            (e.vars) e.rest;
        };
        e = (e.vars (s.type t.p2 e.name)) e.rest;
      };
  } :: (e.vars) e.new-vars,
  e.new-vars : /*empty*/,
  e.vars;

/*
 * Returns the maximum (by length) sequence of cuts contained in t.arg.
 * Cuts are represented by their pragmas.
 * Fails and prints error message if there are unbalanced cuts after '=' or
 * after $error. Prints error message, but not fails if there are unbalanced
 * cuts in negation or trap-sentence.
 */
Get-Cuts t.arg, t.arg : {
  (BRANCH t e.Sentence) = () e.Sentence;
  t.Block = () t.Block;
} $iter {
  e.Sentence : e.Snt t.Statement, {
    t.Statement : \{ (CUTALL t); (ERROR t); } =
      {
        <Print-Error Error! Cut <R 0 e.cuts>> = $fail;
        () e.Snt;
      };
    t.Statement : {
      (CUT t.Pragma) = e.cuts t.Pragma;
      (STAKE t) = { <Middle 0 1 e.cuts>;; };
      (NOT t.Branch) =
        { <Print-Error Error! Cut <R 0 <Get-Cuts t.Branch>>>;; },
        e.cuts;
      (s.block t e.Branches), s.block : \{ BLOCK; BLOCK?; } =
        () e.Branches $iter {
          e.Branches : t.Branch e.rest =
            { <Get-Cuts t.Branch>;; } :: e.branch-cuts,
            {
              <">" (<Length e.branch-cuts>) (<Length e.longest-cuts>)> =
                (e.branch-cuts) e.rest;
              (e.longest-cuts) e.rest;
            };
        } :: (e.longest-cuts) e.Branches,
        e.Branches : /*empty*/ =
        {
          <">" (<Length e.cuts>) (<Length e.longest-cuts>)> =
            e.cuts;
          e.longest-cuts;
        };
      (ITER t.IterBody t.IterVars t.IterCond) =
        <Get-Cuts t.IterCond> :: e.cuts,
        <Get-Cuts t.IterBody> :: e.body-cuts,
        {
          <">" (<Length e.cuts>) (<Length e.body-cuts>)> =
            e.cuts;
          e.body-cuts;
        };
      (TRY t.TryBranch e.NOFAIL t.CatchBlock) =
        { <Print-Error Error! Cut <R 0 <Get-Cuts t.TryBranch>>>;; },
        <Get-Cuts t.CatchBlock>;
//              <Get-Cuts e.CatchSnt> :: e.catch-cuts,
//              {
//                <">" (<Length e.cuts>) (<Length e.catch-cuts>)> =
//                  e.cuts;
//                e.catch-cuts;
//              };
      t.any-other = e.cuts;
    } :: e.cuts,
      (e.cuts) e.Snt;
  };
} :: (e.cuts) e.Sentence,
  e.Sentence : /*empty*/,
  e.cuts;