module Lib.Common

import Prelude
import Data.String
import Data.Int
import Data.SortedMap

record Bounds where
  constructor MkBounds
  startLine : Int
  startCol : Int
  endLine : Int
  endCol : Int

-- FIXME we should handle overlap and out of order..
instance Add Bounds where
  a + b =
    if empty a then b
    else if empty b then a else
    let a' = if a.startLine < b.startLine  || a.startLine == b.startLine && a.startCol < b.startCol then a else b
        b' = if a.endLine < b.endLine || a.endLine == b.endLine && a.endCol < b.endCol then b else a
    in MkBounds a'.startLine a'.startCol b'.endLine b'.endCol
    where
      empty : Bounds → Bool
      empty (MkBounds 0 0 0 0) = True
      empty _ = False

instance Eq Bounds where
  (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
      sl == sl'
   && sc == sc'
   && el == el'
   && ec == ec'

record WithBounds ty where
  constructor MkBounded
  val : ty
  bounds : Bounds

emptyBounds : Bounds
emptyBounds = MkBounds 0 0 0 0

-- l is environment size, this works for both lvl2ix and ix2lvl

range : Int → Int → List Int
range n m = if n < m then n :: range (n + 1) m else Nil

lvl2ix : Int -> Int -> Int
lvl2ix l k = l - k - 1

hexChars : List Char
hexChars = unpack "0123456789ABCDEF"

-- export
hexDigit : Int -> Char
hexDigit v = fromMaybe ' ' (getAt (cast $ mod v 16) hexChars)


toHex : Int -> List Char
toHex 0 = Nil
toHex v = snoc (toHex (div v 16)) (hexDigit v)


quoteString : String -> String
quoteString str = pack $ encode (unpack str) (Lin :<  '"')
  where
    encode : List Char -> SnocList Char -> List Char
    encode Nil acc = acc <>> ('"' :: Nil)
    encode ('"' :: cs) acc = encode cs (acc :< '\\' :< '"')
    encode ('\n' :: cs) acc = encode cs (acc :< '\\' :< 'n')
    encode ('\\' :: cs) acc = encode cs (acc :< '\\' :< '\\')
    encode (c :: cs) acc =
      let v : Int = cast c in
      if v < 32 then encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v )
      else encode cs (acc :< c)


data Json : U where
  JsonObj : List (String × Json) -> Json
  JsonStr : String -> Json
  JsonBool : Bool -> Json
  JsonInt : Int -> Json
  JsonArray : List Json -> Json
  JsonNull : Json


renderJson : Json -> String
renderJson (JsonObj xs) = "{" ++ joinBy "," (map renderPair xs) ++ "}"
  where
    renderPair : (String × Json) -> String
    renderPair (k,v) = quoteString k ++ ":" ++ renderJson v
renderJson (JsonNull) = "null"
renderJson (JsonStr str) = quoteString str
renderJson (JsonBool x) = ite x "true" "false"
renderJson (JsonInt i) = cast i
renderJson (JsonArray xs) = "[" ++ joinBy "," (map renderJson xs) ++ "]"


class ToJSON a where
  toJson : a -> Json


instance ToJSON String where
  toJson = JsonStr


instance ToJSON Int where
  toJson = JsonInt


record FC where
  constructor MkFC
  file : String
  bnds : Bounds


instance Add FC where
  MkFC fn a + MkFC _ b = MkFC fn (a + b)

instance ToJSON FC where
  toJson (MkFC file (MkBounds line col endline endcol)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: ("endline", toJson endline) :: ("endcol", toJson endcol):: Nil)


fcLine : FC -> Int
fcLine fc = fc.bnds.startLine


fcCol : FC -> Int
fcCol fc = fc.bnds.startCol


class HasFC a where
  getFC : a -> FC

primNS : List String
primNS = ("Prim" :: Nil)

emptyFC : FC
emptyFC = MkFC "" (MkBounds 0 0 0 0)

emptyFC' : String → FC
emptyFC' fn = MkFC fn (MkBounds 0 0 0 0)

-- Error of a parse

data QName : U where
  QN : List String -> String -> QName

.baseName : QName → String
(QN _ name).baseName = name

instance Eq QName where
  -- `if` gets us short circuit behavior, idris has a lazy `&&`
  QN ns n == QN ns' n' = if n == n' then ns == ns' else False

instance Show QName where
  show (QN Nil n) = n
  show (QN ns n) = joinBy "." ns ++ "." ++ n

instance Ord QName where
  compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'

data Error
  = E FC String
  | Postpone FC QName String

instance Show FC where
  -- We add one to the end column so it points after the end, which seems to be what Idris does
  show (MkFC file (MkBounds l c el ec)) = "\{file}:\{show $ l + 1}:\{show $ c + 1}--\{show $ el + 1}:\{show $ ec + 2}"

showError : String -> Error -> String
showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src)
  where
    go : Int -> List String -> String
    go l Nil = ""
    go l (x :: xs) =
      if l == fcLine fc then
        let width = fc.bnds.endCol - fc.bnds.startCol + 1 in
        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}\{replicate (cast width) '^'}\n"
      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
      else go (l + 1) xs
showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
  where
    go : Int -> List String -> String
    go l Nil = ""
    go l (x :: xs) =
      if l == fcLine fc then
        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
      else go (l + 1) xs


data Fixity = InfixL | InfixR | Infix


instance Show Fixity where
  show InfixL = "infixl"
  show InfixR = "infixr"
  show Infix = "infix"



record OpDef where
  constructor MkOp
  opname : String
  prec : Int
  fix : Fixity
  isPrefix : Bool
  -- rule is everything after the first part of the operator, splitting on `_`
  -- a normal infix operator will have a trailing `""` which will match to
  -- prec / prec - 1
  rule : List String


Operators : U
Operators = SortedMap String OpDef