quox/lib/Quox/Name.idr

98 lines
1.9 KiB
Idris
Raw Normal View History

2021-07-20 16:05:19 -04:00
module Quox.Name
import public Data.SnocList
2022-05-06 18:57:23 -04:00
import Data.List
2023-03-02 13:52:32 -05:00
import Derive.Prelude
2022-05-13 01:05:55 -04:00
%hide TT.Name
2021-07-20 16:05:19 -04:00
%default total
2022-05-13 01:05:55 -04:00
%language ElabReflection
2021-07-20 16:05:19 -04:00
public export
2022-05-13 01:05:55 -04:00
data BaseName
= UN String -- user-given name
| Unused -- "_"
2023-03-02 13:52:32 -05:00
%runElab derive "BaseName" [Eq, Ord]
2021-07-20 16:05:19 -04:00
export
baseStr : BaseName -> String
baseStr (UN x) = x
baseStr Unused = "_"
2021-07-20 16:05:19 -04:00
export Show BaseName where show = baseStr
export FromString BaseName where fromString = UN
public export
Mods : Type
Mods = SnocList String
2021-07-20 16:05:19 -04:00
public export
record Name where
constructor MakeName
mods : Mods
2021-07-20 16:05:19 -04:00
base : BaseName
2023-03-02 13:52:32 -05:00
%runElab derive "Name" [Eq, Ord]
2021-07-20 16:05:19 -04:00
2023-02-22 01:40:19 -05:00
public export %inline
unq : BaseName -> Name
unq = MakeName [<]
||| add some namespaces to the beginning of a name
public export %inline
addMods : Mods -> Name -> Name
addMods ms = {mods $= (ms <+>)}
public export
PBaseName : Type
PBaseName = String
public export
record PName where
constructor MakePName
mods : Mods
base : String
%runElab derive "PName" [Eq, Ord]
export %inline
fromPName : PName -> Name
fromPName p = MakeName p.mods $ UN p.base
export %inline
toPName : Name -> PName
toPName p = MakePName p.mods $ baseStr p.base
export
Show PName where
show (MakePName mods base) = concat $ intersperse "." $ toList $ mods :< base
export Show Name where show = show . toPName
export FromString PName where fromString = MakePName [<]
export FromString Name where fromString = fromPName . fromString
export
toDotsP : PName -> String
toDotsP x = fastConcat $ cast $ map (<+> ".") x.mods :< x.base
2021-07-20 16:05:19 -04:00
export
toDots : Name -> String
toDots x = fastConcat $ cast $ map (<+> ".") x.mods :< baseStr x.base
2023-02-28 14:51:54 -05:00
export
fromListP : List1 String -> PName
fromListP (x ::: xs) = go [<] x xs where
go : SnocList String -> String -> List String -> PName
go mods x [] = MakePName mods x
2023-02-28 14:51:54 -05:00
go mods x (y :: ys) = go (mods :< x) y ys
export %inline
fromList : List1 String -> Name
fromList = fromPName . fromListP