<commit_before>{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RecordWildCards #-}

module Verifier.SAW.TermNet
  ( Pat(..)
  , Pattern(..)
  , Key
  , key_of_term  -- :: Pat -> [Key]
  , Net          -- :: * -> *
  , empty        -- :: Net a
  , insert       -- :: Eq a => ([Key], a) -> Net a -> Net a
  , insert_term  -- :: (Pattern t, Eq a) => (t, a) -> Net a -> Net a
  , delete       -- :: Eq a => ([Key], a) -> Net a -> Net a
  , delete_term  -- :: (Pattern t, Eq a) => (t, a) -> Net a -> Net a
  , lookup       -- :: Net a -> [Key] -> [a]
  , match_term   -- :: Pattern t => Net a -> t -> [a]
  , unify_term   -- :: Pattern t => Net a -> t -> [a]
  , merge        -- :: Eq a => Net a -> Net a -> Net a
  , content      -- :: Net a -> [a]
  ) where

import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import qualified Data.List as List
import Prelude hiding (lookup)

{-
Based on Pure/net.ML from Isabelle 2012.
Ported from Standard ML to Haskell by <NAME>.

    Title:      Pure/net.ML
    Author:     <NAME>, Cambridge University Computer Laboratory

Discrimination nets: a data structure for indexing items

From the book
    <NAME>, <NAME>, <NAME>.
    Artificial Intelligence Programming.
    (Lawrence Erlbaum Associates, 1980).  [Chapter 14]

match_term no longer treats abstractions as wildcards; instead they match
only wildcards in patterns.  Requires operands to be beta-eta-normal.
-}

-- Laziness is important here, as we will often create and partially
-- traverse patterns for very large terms.
data Pat = Atom String | Var | App Pat Pat

class Pattern t where
  toPat :: t -> Pat

isVarApp :: Pat -> Bool
isVarApp t = case t of
  Atom _   -> False
  Var      -> True
  App t' _ -> isVarApp t'

-- Start
<commit_msg>show instance for term-net pattern type<commit_after>{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RecordWildCards #-}

module Verifier.SAW.TermNet
  ( Pat(..)
  , Pattern(..)
  , Key
  , key_of_term  -- :: Pat -> [Key]
  , Net          -- :: * -> *
  , empty        -- :: Net a
  , insert       -- :: Eq a => ([Key], a) -> Net a -> Net a
  , insert_term  -- :: (Pattern t, Eq a) => (t, a) -> Net a -> Net a
  , delete       -- :: Eq a => ([Key], a) -> Net a -> Net a
  , delete_term  -- :: (Pattern t, Eq a) => (t, a) -> Net a -> Net a
  , lookup       -- :: Net a -> [Key] -> [a]
  , match_term   -- :: Pattern t => Net a -> t -> [a]
  , unify_term   -- :: Pattern t => Net a -> t -> [a]
  , merge        -- :: Eq a => Net a -> Net a -> Net a
  , content      -- :: Net a -> [a]
  ) where

import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import qualified Data.List as List
import Prelude hiding (lookup)

{-
Based on Pure/net.ML from Isabelle 2012.
Ported from Standard ML to Haskell by <NAME>.

    Title:      Pure/net.ML
    Author:     <NAME>, Cambridge University Computer Laboratory

Discrimination nets: a data structure for indexing items

From the book
    <NAME>, <NAME>, <NAME>.
    Artificial Intelligence Programming.
    (Lawrence Erlbaum Associates, 1980).  [Chapter 14]

match_term no longer treats abstractions as wildcards; instead they match
only wildcards in patterns.  Requires operands to be beta-eta-normal.
-}

-- Laziness is important here, as we will often create and partially
-- traverse patterns for very large terms.
data Pat = Atom String | Var | App Pat Pat

class Pattern t where
  toPat :: t -> Pat

instance Show Pat where
  showsPrec p (Atom s) = showString s
  showsPrec p Var = showString "_"
  showsPrec p (App x y) =
      showParen (p > 5) (showsPrec 5 x . showString " " . showsPrec 6 y)

isVarApp :: Pat -> Bool
isVarApp t = case t of
  Atom _   -> False
  Var      -> True
  App t' _ -> isVarApp t'

-- Start

{'fraction_non_alphanumeric': 0.1406209235585703, 'fraction_numerical': 0.006000521784503, 'mean_word_length': 2.3397212543554007, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 76, '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': '4982538', 'n_tokens_mistral': 1329, 'n_tokens_neox': 1267, 'n_words': 484}