<commit_before>{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}

module Render.Concrete where

import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
import Agda.Syntax.Position (noRange)
import Agda.Utils.Float (toStringWithoutDotZero)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor (dget, (<&>))
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Data.Maybe (isNothing, maybeToList)
import qualified Data.Strict.Maybe as Strict
import Render.Class
import Render.Common
import Render.Literal ()
import Render.Name ()
import Render.RichText
import Render.TypeChecking ()

--------------------------------------------------------------------------------

instance Render a => Render (WithHiding a) where
  render w = renderHiding w id $ render $ dget w

-- | OpApp
instance Render (OpApp Expr) where
  render (Ordinary e) = render e
  render (SyntaxBindingLambda r bs e) = render (Lam r bs e)

-- | MaybePlaceholder
instance Render a => Render (MaybePlaceholder a) where
  render Placeholder {} = "_"
  render (NoPlaceholder _ e) = render e

--------------------------------------------------------------------------------

-- | InteractionId
instance Render InteractionId where
  render (InteractionId i) = linkHole i

--------------------------------------------------------------------------------

-- | Expression
instance Render Expr where
  render expr = case expr of
    Ident qname -> render qname
    Lit lit -> render lit
    -- no hole index, use LinkRange instead
    QuestionMark range Nothing -> linkRange range "?"
    QuestionMark _range (Just n) -> linkHole n
    Underscore range n -> linkRange range $ maybe "_" text n
    -- '_range' is almost always 'NoRange' :(
    App _range _ _ ->
      case appView expr of
        AppView e1 args ->
          sepBy " " $ render e1 : map render args
    RawApp _ es -> sepBy " " $ map render es
    OpApp _ q _ es -> sepBy " " $ renderOpApp q es
    WithApp _ e es -> sepBy " | " $ map render (e : es)<commit_msg>[ change ] Display function application with fsep<commit_after>{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}

module Render.Concrete where

import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
import Agda.Syntax.Position (noRange)
import Agda.Utils.Float (toStringWithoutDotZero)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor (dget, (<&>))
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Data.Maybe (isNothing, maybeToList)
import qualified Data.Strict.Maybe as Strict
import Render.Class
import Render.Common
import Render.Literal ()
import Render.Name ()
import Render.RichText
import Render.TypeChecking ()

--------------------------------------------------------------------------------

instance Render a => Render (WithHiding a) where
  render w = renderHiding w id $ render $ dget w

-- | OpApp
instance Render (OpApp Expr) where
  render (Ordinary e) = render e
  render (SyntaxBindingLambda r bs e) = render (Lam r bs e)

-- | MaybePlaceholder
instance Render a => Render (MaybePlaceholder a) where
  render Placeholder {} = "_"
  render (NoPlaceholder _ e) = render e

--------------------------------------------------------------------------------

-- | InteractionId
instance Render InteractionId where
  render (InteractionId i) = linkHole i

--------------------------------------------------------------------------------

-- | Expression
instance Render Expr where
  render expr = case expr of
    Ident qname -> render qname
    Lit lit -> render lit
    -- no hole index, use LinkRange instead
    QuestionMark range Nothing -> linkRange range "?"
    QuestionMark _range (Just n) -> linkHole n
    Underscore range n -> linkRange range $ maybe "_" text n
    -- '_range' is almost always 'NoRange' :(
    App _range _ _ ->
      case appView expr of
        AppView e1 args -> fsep $ render e1 : map render args
    RawApp _ es -> sepBy " " $ map render es
    OpApp _ q _ es -> sepBy " " $ renderOpApp q es
    WithApp _ e es -> sepBy " | " $ map render (e : es)
{'fraction_non_alphanumeric': 0.2006872852233677, 'fraction_numerical': 0.0009163802978235968, 'mean_word_length': 2.2436849925705795, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 29, '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': '2449612', 'n_tokens_mistral': 1235, 'n_tokens_neox': 1238, 'n_words': 413}