<commit_before>{-# LANGUAGE OverlappingInstances, IncoherentInstances, UndecidableInstances,
    PatternGuards, TupleSections #-}

module HerBruijnVal where

import Prelude hiding (pi,abs,mapM,lookup)

import Control.Monad.Reader hiding (mapM)
import Control.Applicative hiding (empty)
import Control.Monad.Error hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.State hiding (mapM)

import Data.Traversable
import Data.Map (Map) 
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe

import Abstract as A
--import Concrete (Name as CName)
import Value
import TypeCheck
-- import Context
import Signature
import Util hiding (lookupSafe)
import Value
import MapEnv as M hiding (mapM)

import Data.Set (Set, empty, notMember, insert)

-- * de Bruijn Terms

data BTm -- names are only used for quoting
  = B Int A.Name
  | BVar A.Name
  | BCon A.Name
  | BDef A.Name
  | BApp BTm BTm
  | BLam A.Name BTm
  | BConstLam BTm -- these are lambdas, but not counted
  | BSort Value.Sort
  | BPi BTm BTm


-- * beta normal values

data HVal
  = HBound Int A.Name [HVal]       -- }   (bound head variable)
  | HVar A.Name HVal  [HVal]       -- }
  | HCon A.Name HVal  [HVal]       -- }-> Head
  | HDef A.Name HVal HVal [HVal]   -- }
  | HLam A.Name HVal
  | HK HVal                        -- constant Lambda, not binding anything and therefor not counted by de Bruijn indices 
  | HSort Value.Sort
  | HFun HVal HVal
  | HDontCare

instance Value A.Name HVal where
  typ = HSort Type
  kind = HSort Kind
  freeVar = var
  valView v =
    case v of
      HBound k name vs    -> VNe name HDontCare (reverse vs) 
      HVar x t vs         -> VNe x t (reverse vs)
      HCon x t vs         -> VNe x t (reverse vs)
      HDef x v t vs       -> VDef x t (reverse vs)
      HLam _ _            -> VAbs
      HK _                -> VAbs
      HSort s             -> VSort s
      HFun a b            -> VPi a b
      -- HDontCare        -> error "Cannot view DontCare Value"
      
      
-- * smart constructors

var :: A.Name -> HVal -> HVal
var x t = HVar x t []

var_ :: A.Name -> HVal
var_ x = var x HDontCare

con :: A.Name -> HVal -> HVal
con x t = HCon x t []

def :: A.Name -> HVal -> HVal -> HVal
def x v t = HDef x v t []


-- * environment handling
-- see MapEnv.hs
type Env' = Env UID HVal

lookupVal :: HVal -> Env' -> HVal
lookupVal v@(HVar x _ _) env = case lookup (uid x) env of
      Just w  -> w
      _       -> v


instance (Applicative m, Monad m, Signature HVal sig, MonadReader sig m) => MonadEval HVal Env' m where

{- THIS IS THE CORRECT CODE -}
  -- apply :: HVal-> HVal -> m HVal
  apply f w =
    case f of
      HBound k name vs            -> return $ HBound k name (w:vs)
      HVar x t vs                 -> return $ HVar x t (w:vs)
      HCon x t vs                 -> return $ HCon x t (w:vs)
      HDef x v t vs               -> return $ HDef x v t (w:vs)
      HLam x v                    -> subst v w
      HK v                        -> return v

{- ONLY FOR DEBUGGING 
  -- apply :: HVal-> HVal -> m HVal
  apply f w = 
    let result = appl' f w
    in 
      (\correctVal -> if checkForPseudofree correctVal then return correctVal else fail $ "APPLY produced a value without unique names") =<< result
    where appl' :: HVal -> HVal -> m HVal
          appl' f w = 
            if (checkForPseudofree f) && (checkForPseudofree w) then
              case f of
                HBound k name vs            -> return $ HBound k name (w:vs)
                HVar x t vs                 -> return $ HVar x t (w:vs)
                HCon x t vs                 -> return $ HCon x t (w:vs)
                HDef x v t vs               -> return $ HDef x v t (w:vs)
                HLam x v                    -> subst v w
                HK v                        -> return v
            else fail $ "APPLY found a value without unique names"
-}
            
{- THIS IS THE CORRECT CODE -}
  -- evaluate :: Expr -> Env' -> m HVal
  evaluate expr env =
    let expr' = transform expr
    in evaluate' expr' env
    where
      -- evaluate' :: BTm -> Env' -> m HVal
      evaluate' btm env = case btm of
        B k n       -> return $ HBound k n []
        BVar x      -> return $ lookupVal (var_ x) env
        BCon x      -> con x . symbType . sigLookup' (uid x) <$> ask
        BDef x      -> do
                      SigDef t v <- sigLookup' (uid x) <$> ask
                      return $ def x v t
        BApp t1 t2  -> Util.appM2 apply (evaluate' t1 env) (evaluate' t2 env)
        BLam x t    -> (\z -> return $ HLam x z) =<< (evaluate' t env)
        BConstLam t -> (\z -> return $ HK z) =<< (evaluate' t env)
        BSort sort  -> return $ HSort sort
        BPi a b     -> Util.appM2 (\a' b' -> return $ HFun a' b') (evaluate' a env) (evaluate' b env)
        

{- THIS IS ONLY FOR DEBUGGING -}
{-  -- evaluate :: Expr -> Env' -> m HVal
  evaluate expr env =
    let expr' = transform expr
        result' = evaluate' expr' env
    in 
    (\correctVal -> if checkForPseudofree correctVal then return correctVal else fail $ "EVALUATE did not bind all variables correctly") =<< result'
    where
      -- evaluate' :: BTm -> Env' -> m HVal
      evaluate' btm env = case btm of
        B k n       -> return $ HBound k n []
        BVar x      -> return $ lookupVal (var_ x) env
        -- BCon x      -> con x . symbType . sigLookup' (uid x) <$> ask
        -- debugging (above is the "normal" code):
        BCon x      -> do
                        result <- con x . symbType . sigLookup' (uid x) <$> ask
                        if checkForPseudofree result then return result else fail $ "EVALUATE: pseudofree variables after BCon"
        BDef x      -> do
                      SigDef t v <- sigLookup' (uid x) <$> ask
                      return $ def x v t
        BApp t1 t2  -> Util.appM2 apply (evaluate' t1 env) (evaluate' t2 env)
        BLam x t    -> (\z -> return $ HLam x z) =<< (evaluate' t env)
        BConstLam t -> (\z -> return $ HK z) =<< (evaluate' t env)
        BSort sort  -> return $ HSort sort
        BPi a b     -> Util.appM2 (\a' b' -> return $ HFun a' b') (evaluate' a env) (evaluate' b env)
-}        

  -- evaluate' :: Expr -> m HVal
  evaluate' = flip evaluate M.empty

  abstractPi a (_, HVar x _ []) b = return $ HFun a $ HLam x $ bindx 0 b where
    bindx :: Int -> HVal -> HVal
    -- debugging
    bindx k (HBound i n vs) = if i<k then HBound i n $ map (bindx k) vs else error "unbound HBound detected"
    bindx k (HVar y t vs)   = (if  x==y 
                                then HBound k x 
                                else HVar y $ bindx k t) 
                                $ map (bindx k) vs
    bindx k (HCon c t vs)   = HCon c t $ map (bindx k) vs
    bindx k (HDef y t d vs) = HDef y t d $ map (bindx k) vs
    bindx k (HLam y t)      = HLam y $ bindx (k+1) t -- wrong: if x==y then HLam y t else HLam y $ bindx (k+1) t
    bindx k (HK t)          = HK $ bindx k t
    bindx k (HFun a b)      = HFun (bindx k a) (bindx k b)
    bindx _ anything        = anything -- Sort, DontCare
  abstractPi _ _ _          = fail $ "can only abstract a free variable"

  unfold v = 
    case v of
      HDef d f t vs   -> appsR f vs
      _               -> return v

  unfolds v = 
    case v of
      HDef d f t vs   -> unfolds =<< appsR' f vs 
      _               -> return v<commit_msg>heads for bound vars in her subst<commit_after>{-# LANGUAGE OverlappingInstances, IncoherentInstances, UndecidableInstances,
    PatternGuards, TupleSections #-}

module HerBruijnVal where

import Prelude hiding (pi,abs,mapM,lookup)

import Control.Monad.Reader hiding (mapM)
import Control.Applicative hiding (empty)
import Control.Monad.Error hiding (mapM)
import Control.Monad.Reader hiding (mapM)
import Control.Monad.State hiding (mapM)

import Data.Traversable
import Data.Map (Map) 
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe

import Abstract as A
--import Concrete (Name as CName)
import Value
import TypeCheck
-- import Context
import Signature
import Util hiding (lookupSafe)
import Value
import MapEnv as M hiding (mapM)

import Data.Set (Set, empty, notMember, insert)

-- * heads

data Head
  = HdBound Int A.Name  -- bound variable: de Bruijn index
  | HdFree A.Name   -- free variable: name
  | HdCon A.Name
  | HdDef A.Name
    deriving (Eq,Ord,Show)

-- * de Bruijn Terms

data BTm -- names are only used for quoting
  = B Int A.Name  -- bound variable: de Bruijn index
  | BVar A.Name   -- free variable: name
  | BCon A.Name
  | BDef A.Name
  | BApp BTm BTm
  | BLam A.Name BTm  -- name irrelevant for execution
  | BConstLam BTm -- these are lambdas, but not counted
  | BSort Value.Sort
  | BPi BTm BTm


-- * beta normal values

data HVal
  = HBound Int A.Name [HVal]       -- }   (bound head variable)
  | HVar A.Name HVal  [HVal]       -- }
  | HCon A.Name HVal  [HVal]       -- }-> Head
  | HDef A.Name HVal HVal [HVal]   -- }
  | HLam A.Name HVal
  | HK HVal                        -- constant Lambda, not binding anything and therefor not counted by de Bruijn indices 
  | HSort Value.Sort
  | HFun HVal HVal
  | HDontCare

instance Value Head HVal where
  typ = HSort Type
  kind = HSort Kind
  freeVar (HdFree x) = var x
  valView v =
    case v of
      HBound k name vs    -> VNe (HdBound k name) HDontCare (reverse vs)
      HVar x t vs         -> VNe (HdFree x) t (reverse vs)
      HCon x t vs         -> VNe (HdCon x) t (reverse vs)
      HDef x v t vs       -> VDef (HdDef x) t (reverse vs)
      HLam _ _            -> VAbs
      HK _                -> VAbs
      HSort s             -> VSort s
      HFun a b            -> VPi a b
      -- HDontCare        -> error "Cannot view DontCare Value"
      
      
-- * smart constructors

var :: A.Name -> HVal -> HVal
var x t = HVar x t []

var_ :: A.Name -> HVal
var_ x = var x HDontCare

con :: A.Name -> HVal -> HVal
con x t = HCon x t []

def :: A.Name -> HVal -> HVal -> HVal
def x v t = HDef x v t []


-- * environment handling
-- see MapEnv.hs
type Env' = Env UID HVal

lookupVal :: HVal -> Env' -> HVal
lookupVal v@(HVar x _ _) env = case lookup (uid x) env of
      Just w  -> w
      _       -> v


instance (Applicative m, Monad m, Signature HVal sig, MonadReader sig m) => MonadEval HVal Env' m where

{- THIS IS THE CORRECT CODE -}
  -- apply :: HVal-> HVal -> m HVal
  apply f w =
    case f of
      HBound k name vs            -> return $ HBound k name (w:vs)
      HVar x t vs                 -> return $ HVar x t (w:vs)
      HCon x t vs                 -> return $ HCon x t (w:vs)
      HDef x v t vs               -> return $ HDef x v t (w:vs)
      HLam x v                    -> subst v w
      HK v                        -> return v

{- ONLY FOR DEBUGGING 
  -- apply :: HVal-> HVal -> m HVal
  apply f w = 
    let result = appl' f w
    in 
      (\correctVal -> if checkForPseudofree correctVal then return correctVal else fail $ "APPLY produced a value without unique names") =<< result
    where appl' :: HVal -> HVal -> m HVal
          appl' f w = 
            if (checkForPseudofree f) && (checkForPseudofree w) then
              case f of
                HBound k name vs            -> return $ HBound k name (w:vs)
                HVar x t vs                 -> return $ HVar x t (w:vs)
                HCon x t vs                 -> return $ HCon x t (w:vs)
                HDef x v t vs               -> return $ HDef x v t (w:vs)
                HLam x v                    -> subst v w
                HK v                        -> return v
            else fail $ "APPLY found a value without unique names"
-}
            
{- THIS IS THE CORRECT CODE -}
  -- evaluate :: Expr -> Env' -> m HVal
  evaluate expr env =
    let expr' = transform expr
    in evaluate' expr' env
    where
      -- evaluate' :: BTm -> Env' -> m HVal
      evaluate' btm env = case btm of
        B k n       -> return $ HBound k n []
        BVar x      -> return $ lookupVal (var_ x) env
        BCon x      -> con x . symbType . sigLookup' (uid x) <$> ask
        BDef x      -> do
                      SigDef t v <- sigLookup' (uid x) <$> ask
                      return $ def x v t
        BApp t1 t2  -> Util.appM2 apply (evaluate' t1 env) (evaluate' t2 env)
        BLam x t    -> (\z -> return $ HLam x z) =<< (evaluate' t env) 
                       -- HLam x <$> evaluate' t env
        BConstLam t -> (\z -> return $ HK z) =<< (evaluate' t env)
        BSort sort  -> return $ HSort sort
        BPi a b     -> Util.appM2 (\a' b' -> return $ HFun a' b') (evaluate' a env) (evaluate' b env)
                       -- HFun <$> evaluate' a env <*> evaluate' b env
        

{- THIS IS ONLY FOR DEBUGGING -}
{-  -- evaluate :: Expr -> Env' -> m HVal
  evaluate expr env =
    let expr' = transform expr
        result' = evaluate' expr' env
    in 
    (\correctVal -> if checkForPseudofree correctVal then return correctVal else fail $ "EVALUATE did not bind all variables correctly") =<< result'
    where
      -- evaluate' :: BTm -> Env' -> m HVal
      evaluate' btm env = case btm of
        B k n       -> return $ HBound k n []
        BVar x      -> return $ lookupVal (var_ x) env
        -- BCon x      -> con x . symbType . sigLookup' (uid x) <$> ask
        -- debugging (above is the "normal" code):
        BCon x      -> do
                        result <- con x . symbType . sigLookup' (uid x) <$> ask
                        if checkForPseudofree result then return result else fail $ "EVALUATE: pseudofree variables after BCon"
        BDef x      -> do
                      SigDef t v <- sigLookup' (uid x) <$> ask
                      return $ def x v t
        BApp t1 t2  -> Util.appM2 apply (evaluate' t1 env) (evaluate' t2 env)
        BLam x t    -> (\z -> return $ HLam x z) =<< (evaluate' t env)
        BConstLam t -> (\z -> return $ HK z) =<< (evaluate' t env)
        BSort sort  -> return $ HSort sort
        BPi a b     -> Util.appM2 (\a' b' -> return $ HFun a' b') (evaluate' a env) (evaluate' b env)
-}        

  -- evaluate' :: Expr -> m HVal
  evaluate' = flip evaluate M.empty

  abstractPi a (_, HVar x _ []) b = return $ HFun a $ HLam x $ bindx 0 b where
    -- INVARIANT in bindx k v: k is bigger than any index in k 
    --   (if k is increased whenever stepping under a lambda)
    bindx :: Int -> HVal -> HVal
    -- debugging
    bindx k (HBound i n vs) = if i<k then HBound i n $ map (bindx k) vs else error "unbound HBound detected"
    bindx k (HVar y t vs)   = (if  x==y 
                                then HBound k x 
                                else HVar y $ bindx k t) 
                                $ map (bindx k) vs
    bindx k (HCon c t vs)   = HCon c t $ map (bindx k) vs
    bindx k (HDef y t d vs) = HDef y t d $ map (bindx k) vs
    bindx k (HLam y t)      = HLam y $ bindx (k+1) t -- wrong: if x==y then HLam y t else HLam y $ bindx (k+1) t
    bindx k (HK t)          = HK $ bindx k t
    bindx k (HFun a b)      = HFun (bindx k a) (bindx k b)
    bindx _ anything        = anything -- Sort, DontCare
  abstractPi _ _ _          = fail $ "can only abstract a free variable"

  unfold v = 
    case v of
      HDef d f t vs   -> appsR f vs
      _               -> return v

  unfolds v = 
    case v of
      HDef d f t vs   -> unfolds =<< appsR' f vs 
      _               -> return v
{'fraction_non_alphanumeric': 0.10004544569239758, 'fraction_numerical': 0.0019476725313250665, 'mean_word_length': 1.579370395177495, 'pattern_counts': {'":': 0, '<': 52, '<?xml version=': 0, '>': 182, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 12, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6469227', 'n_tokens_mistral': 5153, 'n_tokens_neox': 4951, 'n_words': 2055}