<commit_before>{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.CrySAT1 where

import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import qualified Cryptol.TypeCheck.Solver.InfNat as IN
import Text.PrettyPrint
import Data.Maybe(fromMaybe)
import Data.List(unfoldr)
import Control.Monad(liftM, ap)
import qualified Control.Applicative as A


test =
  do -- print (ppExpr expr)
     mapM_ (print . ppProp)
       $ return
       $ crySimplify
       $ expr
  where
  a : b : c : d : _ = map (Var . Name) [ 0 .. ]

  expr = a :== zero
  rest =   Div a b
         : Min (a :* b) (inf :* (inf :* (c :+ d)))
         : []


--------------------------------------------------------------------------------
newtype Name = Name Int
              deriving (Eq,Show)

infixr 2 :||
infixr 3 :&&
infix  4 :==, :>, :>=, :==:, :>:
infixl 6 :+, :-
infixl 7 :*
infixr 8 :^^



-- | Propopsitions, representing Cryptol's numeric constraints (and a bit more).

data Prop = -- Preidcates on natural numbers with infinity.
            Fin Expr
          | Expr :== Expr
          | Expr :>= Expr | Expr :> Expr

          -- Predicate on strict natural numbers (i.e., no infinities)
          | Expr :==: Expr | Expr :>: Expr

          -- Standard logical strucutre
          | Prop :&& Prop | Prop :|| Prop
          | Not Prop
          | PFalse | PTrue
            deriving Show

-- | Expressions, representing Cryptol's numeric types.
data Expr = K Nat'
          | Var Name
          | Expr :+ Expr
          | Expr :- Expr
          | Expr :* Expr
          | Div Expr Expr
          | Mod Expr Expr
          | Expr :^^ Expr
          | Min Expr Expr
          | Max Expr Expr
          | Lg2 Expr
          | Width Expr
          | LenFromThen   Expr Expr Expr
          | LenFromThenTo Expr Expr Expr
            deriving (Eq,Show)

zero :: Expr
zero = K (Nat 0)

one :: Expr
one = K (Nat 1)

inf :: Expr
inf = K Inf



-- | Simplify a property, if possible.
crySimplify :: Prop -> Prop
crySimplify p = last (p : crySimpSteps p)

-- | List the simplification steps for a property.
crySimpSteps :: Prop -> [Prop]
crySimpSteps = unfoldr (fmap dup . crySimpStep)
  where dup x = (x,x)

-- | A single simplification step.
crySimpStep :: Prop -> Maybe Prop
crySimpStep prop =
  case prop of

    Fin x     -> cryIsFin x   -- Fin only on variables.

    x :== y   -> cryIsEq x y
    x :>  y   -> Just (cryIsGt x y)

    x :>= y   ->
      case (x,y) of
        (K (Nat 0), _) -> Just (y :== zero)
        (K Inf, _)     -> Just PTrue
        (_, K Inf)     -> Just (x :== inf)
        _              -> Just (x :== y :|| x :> y)

    x :==: y ->
      case (x,y) of
        (K a, K b)     -> Just (if a == b then PTrue else PFalse)
        (K (Nat 0), _) -> cryIs0 True y
        (_, K (Nat 0)) -> cryIs0 True x
        _ -> bin (:==:) x y

    x :>: y ->
      case x of
        K (Nat 0)   -> Just PFalse
        K (Nat 1)   -> cryIs0 True y
        _           -> bin (:>:) x y

    p :&& q ->
      case cryAnd p q of
        Just r  -> Just r
        Nothing ->
          case crySimpStep p of
            Just p' -> Just (p' :&& q)
            Nothing ->
              case crySimpStep q of
                Just q' -> Just (p :&& q')
                Nothing -> Nothing

    p :|| q ->
      case cryOr p q of
        Just r  -> Just r
        Nothing ->
          case crySimpStep p of
            Just p' -> Just (p' :|| q)
            Nothing ->
              case crySimpStep q of
                Just q' -> Just (p :|| q')
                Nothing -> Nothing

    Not p -> case cryNot p of
               Just r -> Just r
               Nothing ->
                 case crySimpStep p of
                   Just p' -> Just (Not p')
                   Nothing -> Nothing

    PFalse  -> Nothing
    PTrue   -> Nothing

  where
  bin op x y =
    case crySimpExpr x of
      Just x' -> Just (op x' y)
      _ -> case crySimpExpr y of
             Just y' -> Just (op x y')
             Nothing -> Nothing





-- | Simplification of ':&&'.
-- XXX: Add propagation of `let x = t` where x is not in `fvs t`.
cryAnd :: Prop -> Prop -> Maybe Prop
cryAnd p q =
  case p of
    PTrue       -> Just q
    PFalse      -> Just PFalse
    p1 :&& p2   -> Just (p1 :&& (p2 :&& q))

    Not (Fin (Var x))
      | Just q' <- cryKnownFin x False q -> Just (p :&& q')

    Fin (Var x)
      | Just q' <- cryKnownFin x True q -> Just (p :&& q')

    _ -> case q of
           PTrue  -> Just p
           PFalse -> Just PFalse
           _      -> Nothing


cryKnownFin :: Name -> Bool -> Prop -> Maybe Prop
cryKnownFin x isFin prop =
  case prop of
    Fin (Var x') | x == x' -> Just (if isFin then PTrue else PFalse)

    p :&& q -> case (cryKnownFin x isFin p, cryKnownFin x isFin q) of
                 (Nothing, Nothing) -> Nothing
                 (mbP, mbQ) -> Just (fromMaybe p mbP :&& fromMaybe q mbQ)

    p :|| q -> case (cryKnownFin x isFin p, cryKnownFin x isFin q) of
                 (Nothing, Nothing) -> Nothing
                 (mbP, mbQ) -> Just (fromMaybe p mbP :|| fromMaybe q mbQ)

    Not p   -> case cryKnownFin x isFin p of
                 Nothing -> Nothing
                 Just p' -> Just (Not p')

    _ -> Nothing




-- | Simplification of ':||'.
cryOr :: Prop -> Prop -> Maybe Prop
cryOr p q =
  case p of
    PTrue  -> Just PTrue
    PFalse -> Just q
    _ -> case q of
           PTrue  -> Just PTrue
           PFalse -> Just p
           _      -> Nothing


-- | Negation.
cryNot :: Prop -> Maybe Prop
cryNot prop =
  case prop of
    Fin _           -> Nothing

    x :== y         -> Just (x :> y :|| y :> x)
    x :>= y         -> Just (y :>  x)
    x :>  y         -> Just (y :>= x)

    x :==: y        -> Just (x :>: y :|| y :>: x)

    _ :>: _         -> Nothing

    p :&& q         -> Just (Not p :|| Not q)
    p :|| q         -> Just (Not p :&& Not q)
    Not p           -> Just p
    PFalse          -> Just PTrue
    PTrue           -> Just PFalse



-- | Generate a property ensuring that the expression is well-defined.
-- This might be a bit too strict.  For example, we reject things like
-- @max inf (0 - 1)@, which one might think would simplify to @inf@.
cryDefined :: Expr -> Prop
cryDefined expr =
  case expr of
    K _       -> PTrue
    Var _     -> PTrue    -- Variables are always assumed to be OK.
                      -- The idea is that we are going to check for
                      -- defined-ness before instantiating variables.
    x :+ y    -> cryDefined x :&& cryDefined y
    x :- y    -> cryDefined x :&& cryDefined y :&&<commit_msg>Computing free variables, plus some generic traversals.<commit_after>{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.CrySAT1 where

import           Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import qualified Cryptol.TypeCheck.Solver.InfNat as IN
import           Control.Monad(liftM, ap)

import qualified Control.Applicative as A
import           Data.List(unfoldr)
import           Data.Maybe(fromMaybe)
import           Data.Set ( Set )
import qualified Data.Set as Set
import           Text.PrettyPrint

test :: IO ()
test =
  do -- print (ppExpr expr)
     mapM_ (\p -> print (ppProp p) >> putStrLn (replicate 80 '-'))
      $ crySimpSteps
      $ Not (expr :== zero)
  where
  a : b : c : d : _ = map (Var . Name) [ 0 .. ]
  expr = Mod a (b :* inf)
  _rest =  Div a b
         : Min (a :* b) (inf :* (inf :* (c :+ d)))
         : []


--------------------------------------------------------------------------------
newtype Name = Name Int
              deriving (Eq,Ord)

infixr 2 :||
infixr 3 :&&
infix  4 :==, :>, :>=, :==:, :>:
infixl 6 :+, :-
infixl 7 :*
infixr 8 :^^



-- | Propopsitions, representing Cryptol's numeric constraints (and a bit more).

data Prop = -- Preidcates on natural numbers with infinity.
            Fin Expr
          | Expr :== Expr
          | Expr :>= Expr | Expr :> Expr

          -- Predicate on strict natural numbers (i.e., no infinities)
          -- Should be introduced by 'cryNatOp', to eliminte 'inf'.
          | Expr :==: Expr | Expr :>: Expr

          -- Standard logical strucutre
          | Prop :&& Prop | Prop :|| Prop
          | Not Prop
          | PFalse | PTrue

-- | Expressions, representing Cryptol's numeric types.
data Expr = K Nat'
          | Var Name
          | Expr :+ Expr
          | Expr :- Expr
          | Expr :* Expr
          | Div Expr Expr
          | Mod Expr Expr
          | Expr :^^ Expr
          | Min Expr Expr
          | Max Expr Expr
          | Lg2 Expr
          | Width Expr
          | LenFromThen   Expr Expr Expr
          | LenFromThenTo Expr Expr Expr
            deriving Eq

zero :: Expr
zero = K (Nat 0)

one :: Expr
one = K (Nat 1)

inf :: Expr
inf = K Inf


-- | Compute all expressions in a property.
cryPropExprs :: Prop -> [Expr]
cryPropExprs = go []
  where
  go es prop =
    case prop of
      PTrue     -> es
      PFalse    -> es
      Not p     -> go es p
      p :&& q   -> go (go es q) p
      p :|| q   -> go (go es q) p

      Fin x     -> x : es

      x :== y   -> x : y : es
      x :>  y   -> x : y : es
      x :>= y   -> x : y : es

      x :==: y  -> x : y : es
      x :>:  y  -> x : y : es


-- | Compute the immediate sub-expressions of an expression.
cryExprExprs :: Expr -> [Expr]
cryExprExprs expr =
  case expr of
    K _                 -> []
    Var _               -> []
    x :+ y              -> [x,y]
    x :- y              -> [x,y]
    x :* y              -> [x,y]
    Div x y             -> [x,y]
    Mod x y             -> [x,y]
    x :^^ y             -> [x,y]
    Min x y             -> [x,y]
    Max x y             -> [x,y]
    Lg2 x               -> [x]
    Width x             -> [x]
    LenFromThen   x y z -> [x,y,z]
    LenFromThenTo x y z -> [x,y,z]

cryExprFVS :: Expr -> Set Name
cryExprFVS expr =
  case expr of
    Var x -> Set.singleton x
    _     -> Set.unions (map cryExprFVS (cryExprExprs expr))

--------------------------------------------------------------------------------


-- | Simplify a property, if possible.
crySimplify :: Prop -> Prop
crySimplify p = last (p : crySimpSteps p)

-- | List the simplification steps for a property.
crySimpSteps :: Prop -> [Prop]
crySimpSteps = unfoldr (fmap dup . crySimpStep)
  where dup x = (x,x)

-- | A single simplification step.
crySimpStep :: Prop -> Maybe Prop
crySimpStep prop =
  case prop of

    Fin x     -> cryIsFin x   -- Fin only on variables.

    x :== y   -> cryIsEq x y
    x :>  y   -> Just (cryIsGt x y)

    x :>= y   ->
      case (x,y) of
        (K (Nat 0), _) -> Just (y :== zero)
        (K Inf, _)     -> Just PTrue
        (_, K Inf)     -> Just (x :== inf)
        _              -> Just (x :== y :|| x :> y)

    x :==: y ->
      case (x,y) of
        (K a, K b)     -> Just (if a == b then PTrue else PFalse)
        (K (Nat 0), _) -> cryIs0 True y
        (_, K (Nat 0)) -> cryIs0 True x
        _ -> bin (:==:) x y

    x :>: y ->
      case x of
        K (Nat 0)   -> Just PFalse
        K (Nat 1)   -> cryIs0 True y
        _           -> bin (:>:) x y

    p :&& q ->
      case cryAnd p q of
        Just r  -> Just r
        Nothing ->
          case crySimpStep p of
            Just p' -> Just (p' :&& q)
            Nothing ->
              case crySimpStep q of
                Just q' -> Just (p :&& q')
                Nothing -> Nothing

    p :|| q ->
      case cryOr p q of
        Just r  -> Just r
        Nothing ->
          case crySimpStep p of
            Just p' -> Just (p' :|| q)
            Nothing ->
              case crySimpStep q of
                Just q' -> Just (p :|| q')
                Nothing -> Nothing

    Not p -> case cryNot p of
               Just r -> Just r
               Nothing ->
                 case crySimpStep p of
                   Just p' -> Just (Not p')
                   Nothing -> Nothing

    PFalse  -> Nothing
    PTrue   -> Nothing

  where
  bin op x y =
    case crySimpExpr x of
      Just x' -> Just (op x' y)
      _ -> case crySimpExpr y of
             Just y' -> Just (op x y')
             Nothing -> Nothing





-- | Simplification of ':&&'.
-- XXX: Add propagation of `let x = t` where x is not in `fvs t`.
cryAnd :: Prop -> Prop -> Maybe Prop
cryAnd p q =
  case p of
    PTrue       -> Just q
    PFalse      -> Just PFalse
    p1 :&& p2   -> Just (p1 :&& (p2 :&& q))

    Not (Fin (Var x))
      | Just q' <- cryKnownFin x False q -> Just (p :&& q')

    Fin (Var x)
      | Just q' <- cryKnownFin x True q -> Just (p :&& q')

    _ -> case q of
           PTrue  -> Just p
           PFalse -> Just PFalse
           _      -> Nothing


cryKnownFin :: Name -> Bool -> Prop -> Maybe Prop
cryKnownFin x isFin prop =
  case prop of
    Fin (Var x') | x == x' -> Just (if isFin then PTrue else PFalse)

    p :&& q -> case (cryKnownFin x isFin p, cryKnownFin x isFin q) of
                 (Nothing, Nothing) -> Nothing
                 (mbP, mbQ) -> Just (fromMaybe p mbP :&& fromMaybe q mbQ)

    p :|| q -> case (cryKnownFin x isFin p, cryKnownFin x isFin q) of
                 (Nothing, Nothing) -> Nothing
                 (mbP, mbQ) -> Just (fromMaybe p mbP :|| fromMaybe q mbQ)

    Not p   -> case cryKnownFin x isFin p of
                 Nothing -> Nothing
                 Just p' -> Just (Not p')

    _ -> Nothing




-- | Simplification of ':||'.
cryOr :: Prop -> Prop -> Maybe Prop
cryOr p q =
  case p of
    PTrue  -> Just PTrue
    PFalse -> Just q
    _ -> case q of
           PTrue  -> Just PTrue
           PFalse -> Just p
           _      -> Nothing


-- | Negation.
cryNot :: Prop -> Maybe Prop
cryNot prop =
  case prop of
    Fin _           -> Nothing

    x :== y         -> Just (x :> y :|| y :> x)
    x :>= y         -> Just (y :>  x)
    x :>  y         -> Just (y :>= x)

    x :==: y        -> Just (x :>: y :|| y :>: x)

    _ :>: _         -> Nothing

    p :&& q         -> Just (Not p :|| Not q)
    p :|| q         -> Just (Not p :&& Not q)
    Not p           -> Just p
    PFalse          -> Just PTrue
    PTrue           -> Just PFalse




-- | Generate a property ensuring that the expression is well-defined.
-- This might be a bit too strict.  For example, we reject things like
-- @max inf (0 - 1)@, which one might think would simplify to @inf@.
cryDefined :: Expr -> Prop
cryDefined expr =
  case expr of
    K _       -> PTrue
    Var _     -> PTrue    -- Variables are always assumed to be OK.
                      -- The idea is that we are going to check for
                      -- defined-ness before instantiating variables.
    x :+ y    -> cryDefined x :&& cryDefined y
    x :- y    -> cryDefined x :&& cryDefined y :&&
{'fraction_non_alphanumeric': 0.14147669275263694, 'fraction_numerical': 0.003606668935011909, 'mean_word_length': 1.329370740212395, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 269, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4028044', 'n_tokens_mistral': 4990, 'n_tokens_neox': 4693, 'n_words': 1745}