<commit_before>{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, GADTs, ScopedTypeVariables, StandaloneDeriving #-}
module HoleTree where

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    (:::) :: a -> Vec n a -> Vec (S n) a

infixr 5 :::

deriving instance Show a => Show (Vec n a)

data HTree :: Nat -> Nat -> * -> * where
    Leaf :: a -> HTree n n a
    Hole :: HTree (S n) n a
    Fork :: HTree m n a -> HTree n o a -> HTree m o a

deriving instance Show a => Show (HTree m n a)

fill :: Vec m a -> HTree m n a -> (HTree o o a, Vec n a)
fill xs (Leaf x) = (Leaf x, xs)
fill (x ::: xs) Hole = (Leaf x, xs)
fill _ Hole = error "Inaccessible"
fill xs (a `Fork` b) = (a' `Fork` b', xs'')
    where (a', xs') = fill xs a
          (b', xs'') = fill xs' b

fill0 :: Vec m a -> HTree m Z a -> HTree o o a
fill0 xs a = fst (fill xs a)<commit_msg>define an Eq instance by relying a hole-by-hole propositional equality<commit_after>{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, GADTs, ScopedTypeVariables
           , StandaloneDeriving, FlexibleInstances #-}
module HoleTree where

import Data.Type.Equality

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    (:::) :: a -> Vec n a -> Vec (S n) a

infixr 5 :::

deriving instance Show a => Show (Vec n a)

data HTree :: Nat -> Nat -> * -> * where
    Leaf :: a -> HTree n n a
    Hole :: HTree (S n) n a
    Fork :: HTree m n a -> HTree n o a -> HTree m o a

deriving instance Show a => Show (HTree m n a)
instance Eq a => Eq (HTree n m a) where
  Hole == Hole = True
  Leaf a == Leaf b = a == b
  a `Fork` b == a' `Fork` b' | Just Refl <- a `sameHoles` a' = a == a' && b == b'
  _ == _ = False

sameHoles :: HTree m n a -> HTree m n' a -> Maybe (n :~: n')
Hole `sameHoles` Hole = Just Refl
Leaf _ `sameHoles` Leaf _ = Just Refl
a `Fork` b `sameHoles` a' `Fork` b' | Just Refl <- a `sameHoles` a'
                                    , Just Refl <- b `sameHoles` b' = Just Refl
_ `sameHoles` _ = Nothing
infix 4 `sameHoles`

fill :: Vec m a -> HTree m n a -> (HTree o o a, Vec n a)
fill xs (Leaf x) = (Leaf x, xs)
fill (x ::: xs) Hole = (Leaf x, xs)
fill _ Hole = error "Inaccessible"
fill xs (a `Fork` b) = (a' `Fork` b', xs'')
    where (a', xs') = fill xs a
          (b', xs'') = fill xs' b

fill0 :: Vec m a -> HTree m Z a -> HTree o o a
fill0 xs a = fst (fill xs a)
{'fraction_non_alphanumeric': 0.15268456375838926, 'fraction_numerical': 0.002936241610738255, 'mean_word_length': 2.412017167381974, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 38, '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': '4509259', 'n_tokens_mistral': 972, 'n_tokens_neox': 918, 'n_words': 397}