module Core.Name %default total public exportdata Name : Type where     NS : List String -> Name -> Name -- in a namespace     UN : String -> Name -- user defined name     MN : String -> Int -> Name -- machine generated name     PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id     DN : String -> Name -> Name -- a name and how to display it     Nested : (Int, Int) -> Name -> Name -- nested function name     CaseBlock : Int -> Int -> Name -- case block nested in (resolved) name     WithBlock : Int -> Int -> Name -- with block nested in (resolved) name     Resolved : Int -> Name -- resolved, index into context exportuserNameRoot : Name -> Maybe StringuserNameRoot (NS _ n) = userNameRoot nuserNameRoot (UN n) = Just nuserNameRoot (DN _ n) = userNameRoot nuserNameRoot _ = Nothing exportisUserName : Name -> BoolisUserName (PV _ _) = FalseisUserName (MN _ _) = FalseisUserName (NS _ n) = isUserName nisUserName (DN _ n) = isUserName nisUserName _ = True exportnameRoot : Name -> StringnameRoot (NS _ n) = nameRoot nnameRoot (UN n) = nnameRoot (MN n _) = nnameRoot (PV n _) = nameRoot nnameRoot (DN _ n) = nameRoot nnameRoot (Nested _ inner) = nameRoot innernameRoot (CaseBlock n _) = "$" ++ show nnameRoot (WithBlock n _) = "$" ++ show nnameRoot (Resolved i) = "$" ++ show i --- Drop a namespace from a nameexportdropNS : Name -> NamedropNS (NS _ n) = ndropNS n = n exportshowSep : String -> List String -> StringshowSep sep [] = ""showSep sep [x] = xshowSep sep (x :: xs) = x ++ sep ++ showSep sep xs ||| Check whether a given character is a valid identifier characterexportidentChar : Char -> BoolidentChar x = isAlphaNum x || x == '_' || x == '\'' ||  x > chr 127 export Show Name where  show (NS ns n) = showSep "." (reverse ns) ++ "." ++ show n  show (UN x) = x  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"  show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"  show (DN str n) = str  show (Nested (outer, idx) inner)      = show outer ++ ":" ++ show idx ++ ":" ++ show inner  show (CaseBlock outer i) = "case block in " ++ show outer ++ "(" ++ show i ++ ")"  show (WithBlock outer i) = "with block in " ++ show outer  show (Resolved x) = "$resolved" ++ show x exportEq Name where    (==) (NS ns n) (NS ns' n') = n == n' && ns == ns'    (==) (UN x) (UN y) = x == y    (==) (MN x y) (MN x' y') = y == y' && x == x'    (==) (PV x y) (PV x' y') = x == x' && y == y'    (==) (DN _ n) (DN _ n') = n == n'    (==) (Nested x y) (Nested x' y') = x == x' && y == y'    (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'    (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'    (==) (Resolved x) (Resolved x') = x == x'    (==) _ _ = False nameTag : Name -> IntnameTag (NS _ _) = 0nameTag (UN _) = 1nameTag (MN _ _) = 2nameTag (PV _ _) = 3nameTag (DN _ _) = 4nameTag (Nested _ _) = 5nameTag (CaseBlock _ _) = 6nameTag (WithBlock _ _) = 7nameTag (Resolved _) = 8 exportOrd Name where    compare (NS x y) (NS x' y')        = case compare y y' of -- Compare base name first (more likely to differ)               EQ => compare x x'               -- Because of the terrible way Idris 1 compiles 'case', this               -- is actually faster than just having 't => t'...               GT => GT               LT => LT    compare (UN x) (UN y) = compare x y    compare (MN x y) (MN x' y')        = case compare y y' of               EQ => compare x x'               GT => GT               LT => LT    compare (PV x y) (PV x' y')        = case compare y y' of               EQ => compare x x'               GT => GT               LT => LT    compare (DN _ n) (DN _ n') = compare n n'    compare (Nested x y) (Nested x' y')        = case compare y y' of               EQ => compare x x'               GT => GT               LT => LT    compare (CaseBlock x y) (CaseBlock x' y')        = case compare y y' of               EQ => compare x x'               GT => GT               LT => LT    compare (WithBlock x y) (WithBlock x' y')        = case compare y y' of               EQ => compare x x'               GT => GT               LT => LT    compare (Resolved x) (Resolved y) = compare x y     compare x y = compare (nameTag x) (nameTag y) exportnameEq : (x : Name) -> (y : Name) -> Maybe (x = y)nameEq (NS xs x) (NS ys y) with (decEq xs ys)  nameEq (NS ys x) (NS ys y) | (Yes Refl) with (nameEq x y)    nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing    nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl  nameEq (NS xs x) (NS ys y) | (No contra) = NothingnameEq (UN x) (UN y) with (decEq x y)  nameEq (UN y) (UN y) | (Yes Refl) = Just Refl  nameEq (UN x) (UN y) | (No contra) = NothingnameEq (MN x t) (MN x' t') with (decEq x x')  nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t')    nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl    nameEq (MN x t) (MN x t') | (Yes Refl) | (No contra) = Nothing  nameEq (MN x t) (MN x' t') | (No contra) = NothingnameEq (PV x t) (PV y t') with (nameEq x y)  nameEq (PV y t) (PV y t') | (Just Refl) with (decEq t t')    nameEq (PV y t) (PV y t) | (Just Refl) | (Yes Refl) = Just Refl    nameEq (PV y t) (PV y t') | (Just Refl) | (No p) = Nothing  nameEq (PV x t) (PV y t') | Nothing = NothingnameEq (DN x t) (DN y t') with (decEq x y)  nameEq (DN y t) (DN y t') | (Yes Refl) with (nameEq t t')    nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl    nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing  nameEq (DN x t) (DN y t') | (No p) = NothingnameEq (Nested x y) (Nested x' y') with (decEq x x')  nameEq (Nested x y) (Nested x' y') | (No p) = Nothing  nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')    nameEq (Nested x y) (Nested x y') | (Yes Refl) | Nothing = Nothing    nameEq (Nested x y) (Nested x y) | (Yes Refl) | (Just Refl) = Just ReflnameEq (CaseBlock x y) (CaseBlock x' y') with (decEq x x')  nameEq (CaseBlock x y) (CaseBlock x' y') | (No p) = Nothing  nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) with (decEq y y')    nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) | (No p) = Nothing    nameEq (CaseBlock x y) (CaseBlock x y) | (Yes Refl) | (Yes Refl) = Just ReflnameEq (WithBlock x y) (WithBlock x' y') with (decEq x x')  nameEq (WithBlock x y) (WithBlock x' y') | (No p) = Nothing  nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) with (decEq y y')    nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) | (No p) = Nothing    nameEq (WithBlock x y) (WithBlock x y) | (Yes Refl) | (Yes Refl) = Just ReflnameEq (Resolved x) (Resolved y) with (decEq x y)  nameEq (Resolved y) (Resolved y) | (Yes Refl) = Just Refl  nameEq (Resolved x) (Resolved y) | (No contra) = NothingnameEq _ _ = Nothing exportnamesEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)namesEq [] [] = Just ReflnamesEq (x :: xs) (y :: ys)    = do p <- nameEq x y         ps <- namesEq xs ys         rewrite p         rewrite ps         Just ReflnamesEq _ _ = Nothing