• Andrei Paskevich's avatar
    whyml: match expression is ghost if we look inside ghost fields · 43b684d0
    Andrei Paskevich authored
    We store in every lsymbol a new integer field ls_constr,
    equal to zero if the lsymbol is not a constructor, and equal
    to the number of constructors of the lsymbol's type otherwise.
    It is allowed to declare or define an lsymbol with ls_constr > 0
    as an ordinary function (otherwise algebraic type elimination
    wouldn't work - though we might still check this in theories),
    but it is forbidden to use a wrong ls_constr in algebraic type
    The ghostness of a match expression is now determined as follows:
    If at least one branch expression is ghost,
      then the match is ghost;
    else if there is only one branch,
      then the match is not ghost;
    else if the matched expression is ghost,
      then the match is ghost;
    else if at least one pattern matches a ghost field
            against a constructor with ls_constr > 1
      then the match is ghost;
      the match is not ghost.
    We do just enough to recognize obvious non-ghost cases, and
    make no attempt to handle redundant matches or to detect
    exhaustive or-patterns in subpatterns.
pattern.ml 5.58 KB