module Quox.Syntax.Universe

import Quox.Pretty

import Data.Fin
import Derive.Prelude

%default total
%language ElabReflection


||| `UAny` doesn't show up in programs, but when checking something is
||| just some type (e.g. in a signature) it's checked against `Star UAny`
public export
data Universe = U Nat | UAny
%name Universe l

%runElab derive "Universe" [Eq, Ord, Show]

export
PrettyHL Universe where
  prettyM UAny  = pure $ hl Delim "_"
  prettyM (U l) = pure $ hl Free $ pretty l

export
prettyUnivSuffix : Pretty.HasEnv m => Universe -> m (Doc HL)
prettyUnivSuffix UAny  = ifUnicode "_" "₋"
prettyUnivSuffix (U l) =
  ifUnicode (pretty $ pack $ map sub $ unpack $ show l) (pretty l)
 where
  sub : Char -> Char
  sub c = case c of
    '0' => '₀'; '1' => '₁'; '2' => '₂'; '3' => '₃'; '4' => '₄'
    '5' => '₅'; '6' => '₆'; '7' => '₇'; '8' => '₈'; '9' => '₉'; _ => c

export %inline
fromInteger : (x : Integer) -> (0 _ : So (x >= 0)) => Universe
fromInteger x = U $ fromInteger x