/**
 * Format check a term against an RTG
 *
 * This format checker supports any normalized RTG (defined by TATA),
 * including non-deterministic ones. The checker also supports injections.
 *
 * @author  Martin Bravenboer <martin.bravenboer@gmail.com>
 */
module stratego/rtg/format-check
imports
  libstratego-lib
  stratego/rtg/signature
  stratego/rtg/util

/**
 * Main invocation
 */
strategies

  /**
   * Checks that the current term has the format of the given RTG.
   *
   * Fails if the current term has an incorrect format.
   * Does not report errors.
   *
   * @param RTG
   * @type a -> a
   */
  rtg-format-check(|rtg) =
    rtg-format-check(false, true | rtg)
  
  /**
   * Checks that the current term has the format of one of the specified start non-terminals.
   *
   * Fails if the current term has an incorrect format.
   * Does not report errors.
   *
   * @param RTG
   * @type a -> a
   */
  rtg-format-check(|rtg, starts) =
    rtg-format-check(false, true | rtg, starts)
 
  /**
   * Checks that the current term has the format of the given RTG.
   *
   * @param Report errors (true/false)
   * @param Fail if incorrect format (true/false)
   * @param RTG
   * @type a -> a
   */
  rtg-format-check(report-errors, fail-on-error | rtg ) =    
    rtg-format-check(report-errors, fail-on-error | rtg, <?RTG(Start(<id>), _)> rtg)

  /**
   * Checks that the current term has the format of one of the specified start non-terminals.
   *
   * @param Report errors (true/false)
   * @param Fail if incorrect format (true/false)
   * @param RTG
   * @param List(NonTerm)
   * @type a -> a
   */
  rtg-format-check(report-errors, fail-on-error | rtg, starts) =
    where(
      tbl := <new-hashtable>
      ; set := <new-iset>
    )
    ; finally(
        rtgfc-type(|rtg, tbl, set)
        ; if report-errors then    
            where(rtgfc-format-check-report(|rtg, tbl, set))
          end
        ; if fail-on-error then
            where(rtgfc-format-check-error(|starts, tbl, set))
          end
      , <hashtable-destroy> tbl
        ; <iset-destroy> set
      )

strategies

  /**
   * Infers the types of all terms.
   * This strategy does not fail if some of the terms has no type.
   *
   * @param RTG
   */
  rtgfc-type(|rtg, tbl, set) =
    {| rtgfc-InjUserType
     , rtgfc-ListUserType
     , rtgfc-OptUserType
     , rtgfc-TupleUserType
     , rtgfc-IntAppl
     , rtgfc-StringAppl
     , rtgfc-ApplUserType :
      where(<rtgfc-generate-type-rules> rtg)
      ; rtgfc-format-check(|tbl, set)
    |}

  /**
   * Main format check traversal.
   *
   * The first alternatives reuses the result of previous
   * type checking. The size of the traversal is therefore the
   * size of the maximal shared tree.
   *
   * The second alternative tries to infer as many types
   * as possible, but at least one.
   *
   * If this fails, then the term is not in the right format.
   *
   * @type  starts  List(NonTerm)
   */
  rtgfc-format-check(|tbl, set) =
    where(
      <repeat(rtgfc-Type(|tbl, set))> ""
    ; <repeat(rtgfc-Type(|tbl, set))> 0
    )

    ; bottomup-consnil(
         where(rtgfc-get-types(|tbl, set))

      <+ repeat1(rtgfc-Type(|tbl, set))
         ; rtgfc-report-types(|tbl, set)

      <+ one-consnil(not(rtgfc-is-typed(|tbl, set)))

      <+ rtgfc-report-type-failure(id | tbl, set)
      )

  rtgfc-type-string(|tbl, set) =
    is-string; rtgfc-type-special(|"", tbl, set)

  rtgfc-type-int(|tbl, set) =
    is-int; rtgfc-type-special(|0, tbl, set)

  rtgfc-type-special(|special, tbl, set) =
    ?t
    ; where(
        <rtgfc-get-types(|tbl, set)> special => types
      ; <hashtable-put(|t, types)> tbl
      ; <map({type:
          ?type
        ; <iset-add(|(t, type))> set
        })> types
      )

  rtgfc-is-typed(|tbl, set) =
    where(rtgfc-get-types(|tbl, set) => [_ | _])

/**
 * Define type rules for the productions of an RTG.
 *
 * Type rules are defined in a dynamic rule 'UserType'.
 */
strategies

  /**
   * Generate format checking dynamic rules for an RTG
   *
   * @type  RTG -> _
   */
  rtgfc-generate-type-rules =
    rtg-ungroup-productions
    ; ?RTG(Start(_), ProdRules(<id>))
    ; map(rtgfc-generate-type-rule <+ debug(!"internal error: cannot create type rule for "); fail)
    ; if oncetd(?Ref(Int())) then
        rtgfc-generate-type-rule-deprecated-int
      end
    ; if oncetd(?Ref(String())) then
        rtgfc-generate-type-rule-deprecated-string
      end

  /**
   * Int application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(a, [Appl(IntTerm(), [])])
    ; rules(
        rtgfc-IntAppl(|tbl, set) :+ t -> t
        where
          <is-int> t
          ; rtgfc-new-type(|a, tbl, set)
      )

  /**
   * String application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(a, [Appl(StringTerm(), [])])
    ; rules(
        rtgfc-StringAppl(|tbl, set) :+ t -> t
        where
          <is-string> t
          ; rtgfc-new-type(|a, tbl, set)
      )

  /**
   * Deprecated
   */
  rtgfc-generate-type-rule-deprecated-int =
    rules(
      rtgfc-IntAppl(|tbl, set) :+ t -> t
      where
        <is-int> t
        ; rtgfc-new-type(|Int(), tbl, set)
    )

  /**
   * Deprecated
   */
  rtgfc-generate-type-rule-deprecated-string =
    rules(
      rtgfc-StringAppl(|tbl, set) :+ t -> t
      where
        <is-string> t
        ; rtgfc-new-type(|String(), tbl, set)
    )

  /**
   * Injection
   */
  rtgfc-generate-type-rule =
    ?ProdRule(b, [Ref(a)])
    ; rules(
        rtgfc-InjUserType(|tbl, set) :+ t -> t
        where
            <rtgfc-has-type(|a, tbl, set)> t
          ; <not(rtgfc-has-type(|b, tbl, set))> t
          ; <rtgfc-set-type(|b, tbl, set)> t
      )

  /**
   * Cons application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(c, [Appl(ConsTerm(), [Ref(a), Ref(b)])])
    ; rules(
        rtgfc-ListUserType(|tbl, set) :+ t@[hd | tl] -> t
        where
            <rtgfc-has-type(|b, tbl, set)> tl
          ; <not(rtgfc-has-type(|c, tbl, set))> t
          ; <rtgfc-has-type(|a, tbl, set)> hd
          ; <rtgfc-set-type(|c, tbl, set)> t
      )

  /**
   * Conc application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(c, [Appl(ConcTerm(), [Ref(a), Ref(b)])])
    ; rules(
        rtgfc-ListUserType(|tbl, set) :+ t@Conc(t1, t2) -> t
        where
            <rtgfc-has-type(|a, tbl, set)> t1
          ; <rtgfc-has-type(|b, tbl, set)> t2
          ; <rtgfc-new-type(|c, tbl, set)> t
      )

  /**
   * Nil application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(a, [Appl(NilTerm(), [])])
    ; rules(
        rtgfc-ListUserType(|tbl, set) :+ [] -> []
        where
          <rtgfc-new-type(|a, tbl, set)> []
      )

  /**
   * Some application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(b, [Appl(SomeTerm(), [Ref(a)])])
    ; rules(
        rtgfc-OptUserType(|tbl, set) :+ Some(t) -> Some(t)
        where
            <rtgfc-has-type(|a, tbl, set)> t
          ; <rtgfc-new-type(|b, tbl, set)> Some(t)
      )

  /**
   * None application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(a, [Appl(NoneTerm(), [])])
    ; rules(
        rtgfc-OptUserType(|tbl, set) :+ None() -> None()
        where
          <rtgfc-new-type(|a, tbl, set)> None()
      )

  /**
   * Tuple application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(a, [Appl(TupleTerm(_), as)])
    ; where(<map(?Ref(<id>))> as => arg-types)
    ; rules(
        rtgfc-TupleUserType(|tbl, set) :+ t@""#(args) -> t
        where
          <not(rtgfc-has-type(|a, tbl, set))> t
          ; <rtgfc-list-has-type(|arg-types, tbl, set)> args
          ; <rtgfc-set-type(|a, tbl, set)> t
      )

  /**
   * User-defined terminal application
   */
  rtgfc-generate-type-rule =
    ?ProdRule(a, [Appl(Term(f), as)])
    ; where(<map(?Ref(<id>))> as => arg-types)
    ; rules(
        rtgfc-ApplUserType(|tbl, set) :+ t@f#(args) -> t
        where
          <not(rtgfc-has-type(|a, tbl, set))> t
          ; <rtgfc-list-has-type(|arg-types, tbl, set)> args
          ; <rtgfc-set-type(|a, tbl, set)> t
      )

  /**
   * @type  List(_) -> _
   * @type  as  List(NonTerm)
   */
  rtgfc-list-has-type(|as, tbl, set) =
    if ?[] then
      !as => []
    else
      ?[hd | tl]
    ; where(
        !as => [a | bs]
      ; <rtgfc-has-type(|a, tbl, set)> hd
      ; <rtgfc-list-has-type(|bs, tbl, set)> tl
      )
    end

/**
 * Type types a term.
 */
strategies

  rtgfc-Type(|tbl, set) =
    where(
      rtgfc-IntAppl(|tbl, set)
    + rtgfc-StringAppl(|tbl, set)
    + rtgfc-InjUserType(|tbl, set)
    + rtgfc-ApplUserType(|tbl, set)
    + rtgfc-TupleUserType(|tbl, set)
    + rtgfc-ListUserType(|tbl, set)
    + rtgfc-OptUserType(|tbl, set)
    )

strategies

  /**
   * Fails if t already has type nt
   *
   * @type  t -> t
   */
  rtgfc-new-type(|nt, tbl, set) =
    ?term
    ; where(
        not(rtgfc-has-type(|nt, tbl, set))
      ; <hashtable-push(|term, nt)> tbl
      ; <iset-add(|(term, nt))> set
      )

  rtgfc-set-type(|nt, tbl, set) =
    ?term
    ; where(
        <hashtable-push(|term, nt)> tbl
      ; <iset-add(|(term, nt))> set
      )
    
  /**
   * Succeeds if t has type nt
   *
   * @type  t -> t
   */
  rtgfc-has-type(|nt, tbl, set) =
    ?term
    ; not(is-string + is-int)
    ; where(
        <iset-contains(|(term, nt))> set
      )

  rtgfc-has-type(|nt, tbl, set) =
    is-int
    ; where(<iset-contains(|(0, nt))> set)

  rtgfc-has-type(|nt, tbl, set) =
    is-string
    ; where(<iset-contains(|("", nt))> set)

  rtgfc-retrieve-types(|tbl, set) =
    rtgfc-get-types(|tbl, set)
    <+ ?t
       ; where(
           <hashtable-put(|t, [])> tbl
         )
       ; ![]

  rtgfc-get-types(|tbl, set) =
    ?t
    ; not(is-string + is-int)
    ; <hashtable-get(|t)> tbl

  rtgfc-get-types(|tbl, set) =
    is-int
    ; <hashtable-get(|0)> tbl

  rtgfc-get-types(|tbl, set) =
    is-string
    ; <hashtable-get(|"")> tbl

/**
 * Reporting
 */
strategies


  /**
   * @param RTG or List(NonTerm)
   */    
  rtgfc-format-check-error(|rtg, tbl, set) =
    where(starts := <?RTG(Start(<id>), _) <+ is-list> rtg)  
    ; where(
        types := <rtgfc-get-types(|tbl, set) <+ ![]>
        ; if <isect> (starts, types) => [] then
            fail
          end
      )

  /**
   * @param RTG
   */
  rtgfc-format-check-report(|rtg, tbl, set) =
    where(starts := <?RTG(Start(<id>), _)> rtg)
    ; rtgfc-format-check-report(|starts, tbl ,set)

  /**
   * @param List(NonTerm)
   */
  rtgfc-format-check-report(|starts, tbl, set) =
    where(
      <is-list> starts
    ; (rtgfc-get-types(|tbl, set) <+ ![]) => types
    ; if !types => [] then
        !1 // already reported <fatal-error> ["error: term cannot be typed."]
      else
          <isect> (starts, <id>)
        ; if ?[] then
	    if-verbose1(
              <fprintnl> (<stderr-stream>,
                ["error: term typed as ", <rtgfc-types-to-string> types, 
                 " but expected ", <rtgfc-types-to-string> starts])
            )
            ; !1
          else
            if-verbose2(
              <rtgfc-types-to-string; debug(!"info: term typed as ")> types
            )
            ; !0
          end
      end
    ; <set-config> ("--exit-code", <id>)
    )

  rtgfc-report-types(|tbl, set) = if-verbose2(
    ?term
    ; where(
        rtgfc-get-types(|tbl, set)
      ; switch id
          case ?[] :
            !["  Cannot type ", term]
          case ?[t] :
            !["  Typed ", <write-to-string> term, " as ", <rtgfc-nonterm-to-string> t]
          otherwise:
            !["  Typed ", <write-to-string> term, " as one of ", <rtgfc-types-to-string>]
        end
     ; <fprintnl> (<stderr-stream>, <id>)
     )
   )
  
  rtgfc-report-type-failure(finally | tbl, set) =
    ?t
    ; where(
        <fprintnl> (<stderr-stream>, ["error: cannot type ", <write-to-string>])
      )
    ; if <one-consnil(id)> t then
        <fprintnl> (<stderr-stream>, ["    inferred types of subterms: "])
      ; <all-consnil(
          where(
            <fprintnl> (<stderr-stream>, ["    typed ", <write-to-string>, " as ", <rtgfc-retrieve-types(|tbl, set); rtgfc-types-to-string>])
          )
        )> t
      else id end
    ; finally

  rtgfc-nonterm-to-string =
    ?Set(<rtgfc-types-to-string>) <+ rtg-to-string

  rtgfc-types-to-string =
    map(rtg-to-string); separate-by(!", "); concat-strings

  rtg-to-string :
    Int() -> ""

  rtg-to-string :
    String() -> ""

strategies

  /**
   * @type  List(a) -> List(b)
   * @type  s List(a) -> b
   */
  map-consnil(s) =
    rec x({tail:
      ?[_ | tail]
    ; s
    ; ![<id> | <x> tail]
    <+ []
    })

  /**
   * bttomup variant that traverses lists as cons/nil.
   */
  bottomup-consnil(s) =
    rec x(all-consnil(x); s)

  /**
   * all variant that traverses lists as cons/nil.
   */
  all-consnil(s) = 
    is-list < ([s | s] + []) + all(s)

  /**
   * one variant that traverses lists as cons/nil.
   */
  one-consnil(s) = 
    is-list < ([s | id] + [id | s]) + one(s)