<commit_before><commit_msg>Forgot to add file SAW/Module.hs<commit_after>{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}

{- |
Module      : Verifier.SAW.Module
Copyright   : Galois, Inc. 2012-2017
License     : BSD3
Maintainer  : <EMAIL>
Stability   : experimental
Portability : non-portable (language extensions)
-}

module Verifier.SAW.Module
  ( -- * Patterns.
    Pat(..)
  , patBoundVars
  , patBoundVarCount
  , patUnusedVarCount
    -- * Data types and definitions.
  , DefQualifier(..)
  , Def(..)
  , DefEqn(..)
  , Ctor(..)
  , DataType(..)
  ) where

import Control.Lens
#if !MIN_VERSION_base(4,8,0)
import Data.Foldable (Foldable)
#endif
import Data.Hashable
import GHC.Generics (Generic)

import Prelude hiding (all, foldr, sum)

import Verifier.SAW.Term.Functor
import Verifier.SAW.Utils (sumBy)

-- Patterns --------------------------------------------------------------------

-- Patterns are used to match equations.
data Pat e = -- | Variable bound by pattern.
             -- Variables may be bound in context in a different order than
             -- a left-to-right traversal.  The DeBruijnIndex indicates the order.
             PVar String DeBruijnIndex e
             -- | The
           | PUnused DeBruijnIndex e
           | PUnit
           | PPair (Pat e) (Pat e)
           | PEmpty
           | PField (Pat e) (Pat e) (Pat e) -- ^ Field name, field value, rest of record
           | PString String
           | PCtor Ident [Pat e]
  deriving (Eq,Ord, Show, Functor, Foldable, Traversable, Generic)

instance Hashable e => Hashable (Pat e) -- automatically derived

patBoundVarCount :: Pat e -> DeBruijnIndex
patBoundVarCount p =
  case p of
    PVar{} -> 1
    PUnused{} -> 0
    PCtor _ l -> sumBy patBoundVarCount l
    PUnit     -> 0
    PPair x y -> patBoundVarCount x + patBoundVarCount y
    PEmpty    -> 0
    PField f x y -> patBoundVarCount f + patBoundVarCount x + patBoundVarCount y
    PString _ -> 0

patUnusedVarCount :: Pat e -> DeBruijnIndex
patUnusedVarCount p =
  case p of
    PVar{}       -> 0
    PUnused{}    -> 1
    PCtor _ l    -> sumBy patUnusedVarCount l
    PUnit        -> 0
    PPair x y    -> patUnusedVarCount x + patUnusedVarCount y
    PEmpty       -> 0
    PField _ x y -> patUnusedVarCount x + patUnusedVarCount y
    PString _    -> 0

patBoundVars :: Pat e -> [String]
patBoundVars p =
  case p of
    PVar s _ _   -> [s]
    PCtor _ l    -> concatMap patBoundVars l
    PUnit        -> []
    PPair x y    -> patBoundVars x ++ patBoundVars y
    PEmpty       -> []
    PField _ x y -> patBoundVars x ++ patBoundVars y
    PString _    -> []
    PUnused{}    -> []


-- Definitions -----------------------------------------------------------------

data DefQualifier
  = NoQualifier
  | PrimQualifier
  | AxiomQualifier
 deriving (Eq, Ord, Show, Generic)

instance Hashable DefQualifier -- automatically derived

-- | A Definition contains an identifier, the type of the definition, and a list of equations.
data Def e =
  Def
  { defIdent :: Ident
  , defQualifier :: DefQualifier
  , defType :: e
  , defEqs :: [DefEqn e]
  }
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic)

instance (Hashable e) => Hashable (Def e) -- automatically derived

data DefEqn e
  = DefEqn [Pat e] e -- ^ List of patterns and a right hand side
  deriving (Functor, Foldable, Traversable, Generic, Show)

instance Hashable e => Hashable (DefEqn e) -- automatically derived

instance (Eq e) => Eq (DefEqn e) where
  DefEqn xp xr == DefEqn yp yr = xp == yp && xr == yr

instance (Ord e) => Ord (DefEqn e) where
  compare (DefEqn xp xr) (DefEqn yp yr) = compare (xp,xr) (yp,yr)


-- Constructors ----------------------------------------------------------------

data Ctor tp =
  Ctor
  { ctorName :: !Ident
  , ctorType :: tp -- ^ The type of the constructor (should contain no free variables).
  }
  deriving (Functor, Foldable, Traversable)

lift2 :: (a -> b) -> (b -> b -> c) -> a -> a -> c
lift2 f h x y = h (f x) (f y)

instance Eq (Ctor tp) where
  (==) = lift2 ctorName (==)

instance Ord (Ctor tp) where
  compare = lift2 ctorName compare

instance Show (Ctor tp) where
  show = show . ctorName


-- Datatypes -------------------------------------------------------------------

data DataType t =
  DataType
  { dtName :: Ident
  , dtType :: t
  , dtCtors :: [Ctor t]
  , dtIsPrimitive :: Bool
  }
  deriving (Functor, Foldable, Traversable)

instance Eq (DataType t) where
  (==) = lift2 dtName (==)

instance Ord (DataType t) where
  compare = lift2 dtName compare

instance Show (DataType t) where
  show = show . dtName
{'fraction_non_alphanumeric': 0.15938303341902313, 'fraction_numerical': 0.005998286203941731, 'mean_word_length': 2.0982083609820834, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 43, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2103314', 'n_tokens_mistral': 1554, 'n_tokens_neox': 1530, 'n_words': 498}