<commit_before>{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, StandaloneDeriving, GADTs,
             MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
             UndecidableInstances, TypeHoles, TypeFamilies #-}

-- See: https://code.google.com/p/omega/wiki/LambdaGraph
-- TODO: model "let(rec) a = sub in expr" with KILL1 @ sub (expr ... UP LEFT)
-- TODO: use Maybe instead of NoWay

data {-kind-} Lam = App Lam Lam | Abs Lam | Ref [Go]
data {-kind-} Go = Up | Le | Ri | Down

data {-kind-} Trace = Root Lam | AppL Trace Lam | AppR Trace Lam | AbsD Trace Lam

-- a zipper for lambda trees
--
data Traced :: (Lam -> *) -> Trace -> * where
  EmptyRoot :: Builder l => l sh -> Traced l (Root sh)
  AppLeft :: Builder l => Traced l tr -> l (App shl shr) -> Traced l (AppL tr shl)
  AppRight :: Builder l => Traced l tr -> l (App shl shr) -> Traced l (AppR tr shr)
  AbsDown :: Builder l => Traced l tr -> l (Abs sh) -> Traced l (AbsD tr sh)

deriving instance Show (Traced Classical tr)

class Builder (shape :: Lam -> *) where
  lam :: shape inner -> shape (Abs inner)
  app :: shape left -> shape right -> shape (App left right)
  here :: shape (Ref '[Up])
  up :: shape (Ref p) -> shape (Ref (Up ': p))
  close :: Closed sh env => Traced shape env -> shape sh -> shape sh
  close _ sh = sh
  checkClosure :: Traced shape env -> shape sh -> Proven sh env

class Closed (sh :: Lam) (env :: Trace)
instance Closed (Ref '[]) env
instance Closed (Ref more) up => Closed (Ref (Up ': more)) ((down :: Trace -> Lam -> Trace) up sh)

type family Shape (env :: Trace) :: Lam
type instance Shape (Root sh) = sh
type instance Shape ((down :: Trace -> Lam -> Trace) up sh) = sh

instance CanGo (Le ': more) (Shape env) => Closed (Ref (Le ': more)) env
instance CanGo (Ri ': more) (Shape env) => Closed (Ref (Ri ': more)) env
instance CanGo (Down ': more) (Shape env) => Closed (Ref (Down ': more)) env

class CanGo (down :: [Go]) (from :: Lam)
instance CanGo '[] sh
instance CanGo more l => CanGo (Le ': more) (App l r)
instance CanGo more r => CanGo (Ri ': more) (App l r)
instance CanGo more d => CanGo (Down ': more) (Abs d)


instance Closed below (AbsD env below) => Closed (Abs below) env
instance (Closed left (AppL env left), Closed right (AppR env right)) => Closed (App left right) env

data Proven :: Lam -> Trace -> * where
  NoWay :: Proven sh env
  TrivialRef :: Proven (Ref '[]) env
  ProvenRefUp :: Closed (Ref more) env => Proven (Ref more) env -> Proven (Ref (Up ': more)) ((down :: Trace -> Lam -> Trace) env stuff)
  ProvenRefLeft :: CanGo more (Shape env) => Proven (Ref more) (AppL env stuff) -> Proven (Ref (Le ': more)) env
  ProvenRefRight :: CanGo more (Shape env) => Proven (Ref more) (AppR env stuff) -> Proven (Ref (Ri ': more)) env
  ProvenRefDown :: CanGo more (Shape env) => Proven (Ref more) (AbsD env stuff) -> Proven (Ref (Down ': more)) env
  ProvenApp :: (Closed l (AppL env l), Closed r (AppR env r)) =>
               Proven l (AppL env l) -> Proven r (AppR env r) ->
               Proven (App l r) env
  ProvenAbs :: Closed below (AbsD env below) =>
               Proven below (AbsD env below) -> Proven (Abs below) env

deriving instance Show (Proven sh env)

getShape :: Traced Classical env -> Classical (Shape env)
getShape (EmptyRoot a@(APP _ _)) = a
getShape (EmptyRoot a@(LAM _)) = a
getShape (AppLeft _ (APP l _)) = l
getShape (AppRight _ (APP _ r)) = r
getShape (AbsDown _ (LAM d)) = d


type family AppLShape (env :: Trace) :: Trace
type instance AppLShape (Root (App l r)) = AppL (Root (App l r)) l
type instance AppLShape (AbsD up (App l r)) = AppL (AbsD up (App l r)) l
type instance AppLShape (AppL up (App l r)) = AppL (AppL up (App l r)) l
type instance AppLShape (AppR up (App l r)) = AppL (AppR up (App l r)) l


proveRefLeft :: Classical (Ref (Le ': more)) -> Traced Classical env -> Proven (Ref (Le ': more)) env
proveRefLeft (LEFT more) env = case relevantLeft env of
                               Nothing -> NoWay
                               Just down -> case proveRef more down of
                                            NoWay -> NoWay
                                            p@TrivialRef -> ProvenRefLeft p


relevantLeft :: Traced Classical env -> Maybe (Traced Classical (AppLShape env))
relevantLeft env@(EmptyRoot a@(APP _ _)) = Just $ AppLeft env a
relevantLeft env@(AbsDown _ (LAM a@(APP _ _))) = Just $ AppLeft env a
relevantLeft env@(AppLeft _ (APP a@(APP _ _) _)) = Just $ AppLeft env a
relevantLeft env@(AppRight _ (APP _ a@(APP _ _))) = Just $ AppLeft env a
relevantLeft _ = Nothing


-- prove a Ref by looking at last *step* where we passed by
--
proveRef :: Classical (Ref more) -> Traced Classical env -> Proven (Ref more) env
proveRef HERE (AbsDown _ _) = ProvenRefUp TrivialRef
proveRef HERE (AppLeft _ _) = ProvenRefUp TrivialRef
proveRef HERE (AppRight _ _) = ProvenRefUp TrivialRef
proveRef STOP _ = TrivialRef
proveRef l@(LEFT more) env = proveRefLeft l env -- case relevantLeft env of
                           --Nothing -> NoWay
                           --Just down -> case proveRef more down of
                           --             NoWay -> NoWay
                                      --  p@TrivialRef -> ProvenRefLeft p<commit_msg>WIP: hold up some more equality evidence<commit_after>{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, StandaloneDeriving, GADTs,
             MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
             UndecidableInstances, TypeHoles, TypeFamilies #-}

-- See: https://code.google.com/p/omega/wiki/LambdaGraph
-- TODO: model "let(rec) a = sub in expr" with KILL1 @ sub (expr ... UP LEFT)
-- TODO: use Maybe instead of NoWay

data {-kind-} Lam = App Lam Lam | Abs Lam | Ref [Go]
data {-kind-} Go = Up | Le | Ri | Down

data {-kind-} Trace = Root Lam | AppL Trace Lam | AppR Trace Lam | AbsD Trace Lam

-- a zipper for lambda trees
--
data Traced :: (Lam -> *) -> Trace -> * where
  EmptyRoot :: Builder l => l sh -> Traced l (Root sh)
  AppLeft :: Builder l => Traced l tr -> l (App shl shr) -> Traced l (AppL tr shl)
  AppRight :: Builder l => Traced l tr -> l (App shl shr) -> Traced l (AppR tr shr)
  AbsDown :: Builder l => Traced l tr -> l (Abs sh) -> Traced l (AbsD tr sh)

deriving instance Show (Traced Classical tr)

class Builder (shape :: Lam -> *) where
  lam :: shape inner -> shape (Abs inner)
  app :: shape left -> shape right -> shape (App left right)
  here :: shape (Ref '[Up])
  up :: shape (Ref p) -> shape (Ref (Up ': p))
  close :: Closed sh env => Traced shape env -> shape sh -> shape sh
  close _ sh = sh
  checkClosure :: Traced shape env -> shape sh -> Proven sh env

class Closed (sh :: Lam) (env :: Trace)
instance Closed (Ref '[]) env
instance Closed (Ref more) up => Closed (Ref (Up ': more)) ((down :: Trace -> Lam -> Trace) up sh)

type family Shape (env :: Trace) :: Lam
type instance Shape (Root sh) = sh
type instance Shape ((down :: Trace -> Lam -> Trace) up sh) = sh

instance CanGo (Le ': more) (Shape env) => Closed (Ref (Le ': more)) env
instance CanGo (Ri ': more) (Shape env) => Closed (Ref (Ri ': more)) env
instance CanGo (Down ': more) (Shape env) => Closed (Ref (Down ': more)) env

class CanGo (down :: [Go]) (from :: Lam)
instance CanGo '[] sh
instance CanGo more l => CanGo (Le ': more) (App l r)
instance CanGo more r => CanGo (Ri ': more) (App l r)
instance CanGo more d => CanGo (Down ': more) (Abs d)


instance Closed below (AbsD env below) => Closed (Abs below) env
instance (Closed left (AppL env left), Closed right (AppR env right)) => Closed (App left right) env

data Proven :: Lam -> Trace -> * where
  NoWay :: Proven sh env
  TrivialRef :: Proven (Ref '[]) env
  ProvenRefUp :: Closed (Ref more) env => Proven (Ref more) env -> Proven (Ref (Up ': more)) ((down :: Trace -> Lam -> Trace) env stuff)
  ProvenRefLeft :: CanGo more (Shape env) => Proven (Ref more) (AppL env stuff) -> Proven (Ref (Le ': more)) env
  ProvenRefRight :: CanGo more (Shape env) => Proven (Ref more) (AppR env stuff) -> Proven (Ref (Ri ': more)) env
  ProvenRefDown :: CanGo more (Shape env) => Proven (Ref more) (AbsD env stuff) -> Proven (Ref (Down ': more)) env
  ProvenApp :: (Closed l (AppL env l), Closed r (AppR env r)) =>
               Proven l (AppL env l) -> Proven r (AppR env r) ->
               Proven (App l r) env
  ProvenAbs :: Closed below (AbsD env below) =>
               Proven below (AbsD env below) -> Proven (Abs below) env

deriving instance Show (Proven sh env)

{-
getShape :: Traced Classical env -> Classical (Shape env)
getShape (EmptyRoot a@(APP _ _)) = a
getShape (EmptyRoot a@(LAM _)) = a
getShape (AppLeft _ (APP l _)) = l
getShape (AppRight _ (APP _ r)) = r
getShape (AbsDown _ (LAM d)) = d
-}


type family AppLShape (env :: Trace) :: Trace
type instance AppLShape (Root (App l r)) = AppL (Root (App l r)) l
type instance AppLShape (AbsD up (App l r)) = AppL (AbsD up (App l r)) l
type instance AppLShape (AppL up (App l r)) = AppL (AppL up (App l r)) l
type instance AppLShape (AppR up (App l r)) = AppL (AppR up (App l r)) l


proveRefLeft :: Classical (Ref (Le ': more)) -> Traced Classical env -> Proven (Ref (Le ': more)) env
proveRefLeft (LEFT more) env = case relevantLeft env of
                               Nothing -> NoWay
                               Just (down@(AppLeft _ _), Lefty _ _) -> case proveRef more down of
                                                          NoWay -> NoWay
                                                          p@TrivialRef -> ProvenRefLeft p
                                                          --p@(ProvenRefLeft _) -> ProvenRefLeft p

data SameShape :: Trace -> * where
  Lefty :: (AppLShape env ~ AppL env sh) => Traced l (AppLShape env) -> Traced l (AppL env sh) -> SameShape env


relevantLeft :: Traced Classical env -> Maybe (Traced Classical (AppLShape env), SameShape env)
relevantLeft env@(EmptyRoot a@(APP _ _)) = Just $ (AppLeft env a, Lefty (AppLeft env a) (AppLeft env a))
relevantLeft env@(AbsDown _ (LAM a@(APP _ _))) = Just $ (AppLeft env a, Lefty (AppLeft env a) (AppLeft env a))
relevantLeft env@(AppLeft _ (APP a@(APP _ _) _)) = Just $ (AppLeft env a, Lefty (AppLeft env a) (AppLeft env a))
relevantLeft env@(AppRight _ (APP _ a@(APP _ _))) = Just $ (AppLeft env a, Lefty (AppLeft env a) (AppLeft env a))
relevantLeft _ = Nothing


-- prove a Ref by looking at last *step* where we passed by
--
proveRef :: Classical (Ref more) -> Traced Classical env -> Proven (Ref more) env
proveRef HERE (AbsDown _ _) = ProvenRefUp TrivialRef
proveRef HERE (AppLeft _ _) = ProvenRefUp TrivialRef
proveRef HERE (AppRight _ _) = ProvenRefUp TrivialRef
proveRef STOP _ = TrivialRef
proveRef l@(LEFT more) env = proveRefLeft l env -- case relevantLeft env of
                           --Nothing -> NoWay
                           --Just down -> case proveRef more down of
                           --             NoWay -> NoWay
                                      --  p@TrivialRef -> ProvenRefLeft p
{'fraction_non_alphanumeric': 0.12795132582637123, 'fraction_numerical': 0.00018162005085361425, 'mean_word_length': 2.674674674674675, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 144, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 19, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1424592', 'n_tokens_mistral': 3582, 'n_tokens_neox': 3435, 'n_words': 1454}