{-# LANGUAGE PatternSynonyms #-}
module Syntax where

import Data.Function (on)
import Data.Text (Text)

import Presyntax.Presyntax (Plicity(..))
import qualified Data.Text as T
import Data.IORef (IORef)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

data WiredIn
  = WiType
  | WiPretype
  | WiInterval
  | WiI0
  | WiI1
  | WiIAnd
  | WiIOr
  | WiINot
  | WiPathP

  | WiIsOne   -- Proposition associated with an element of the interval
  | WiItIsOne -- 1 = 1
  | WiIsOne1  -- i j -> [i] -> [ior i j]
  | WiIsOne2  -- i j -> [j] -> [ior i j]

  | WiPartial  -- (φ : I) -> Type           -> Typeω
  | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
  deriving (Eq, Show, Ord)

data Term
  = Ref  Name
  | App  Plicity Term Term
  | Lam  Plicity Text Term
  | Pi   Plicity Text Term Term
  | Meta MV
  | Type
  | Typeω

  | Sigma Text Term Term
  | Pair Term Term
  | Proj1 Term
  | Proj2 Term

  | I
  | I0 | I1
  | IAnd Term Term
  | IOr  Term Term
  | INot Term

  | PathP     Term Term Term
  -- ^ PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
  | IElim     Term Term Term Term Term
  -- ^ IElim : {A : I -> Type} {x : A i0} {y : A i1} (p : PathP A x y) (i : I) -> A i
  | PathIntro Term Term
  -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
  --   ~~~~~~~~~ not printed at all

  | IsOne Term
  | IsOne1 Term
  | IsOne2 Term
  | ItIsOne

  | Partial  Term Term
  | PartialP Term Term

  | System (Map Term Term)
  deriving (Eq, Show, Ord)

data MV =
  MV { mvName :: Text
     , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
     }

instance Eq MV where
  (==) = (==) `on` mvName
instance Ord MV where
  (<=) = (<=) `on` mvName
instance Show MV where
  show = ('?':) . T.unpack . mvName

data Name
  = Bound   Text
  | Defined Text
  deriving (Eq, Show, Ord)

type NFType = Value
type NFEndp = Value

data Value
  = VNe    Head            (Seq Projection)
  | VLam   Plicity         Closure
  | VPi    Plicity Value   Closure
  | VSigma Value   Closure
  | VPair  Value   Value

  | VType | VTypeω

  | VI
  | VI0 | VI1
  | VIAnd Value Value
  | VIOr  Value Value
  | VINot Value

  | VPath Value Value Value
  | VLine Value Value

  | VIsOne Value
  | VItIsOne
  | VIsOne1 Value
  | VIsOne2 Value

  | VPartial NFEndp Value
  | VPartialP NFEndp Value
  | VSystem (Map Value Value)
  deriving (Eq, Show, Ord)

pattern VVar :: Name -> Value
pattern VVar x = VNe (HVar x) Seq.Empty

quoteWith :: Set Text -> Value -> Term
quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
  goHead (HVar v) = Ref v
  goHead (HMeta m) = Meta m

  goSpine t (PApp p v)       = App p t (quoteWith names v)
  goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i)
  goSpine t PProj1 = Proj1 t
  goSpine t PProj2 = Proj2 t

quoteWith names (VLam p (Closure n k)) =
  let n' = refresh names n
   in Lam p n' (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))

quoteWith names (VPi p d (Closure n k)) =
  let n' = refresh names n
   in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))

quoteWith names (VSigma d (Closure n k)) =
  let n' = refresh names n
   in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))

quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
quoteWith _ VType = Type
quoteWith _ VTypeω = Typeω

quoteWith _ VI     = I
quoteWith _ VI0    = I0
quoteWith _ VI1    = I1
quoteWith names (VIAnd x y) = IAnd (quoteWith names x) (quoteWith names y)
quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
quoteWith names (VINot x) = INot (quoteWith names x)

quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
quoteWith names (VLine p f)      = PathIntro (quoteWith names p) (quoteWith names f)

quoteWith names (VIsOne v)  = IsOne (quoteWith names v)
quoteWith names (VIsOne1 v) = IsOne1 (quoteWith names v)
quoteWith names (VIsOne2 v) = IsOne2 (quoteWith names v)
quoteWith _     VItIsOne    = ItIsOne

quoteWith names (VPartial x y) = Partial (quoteWith names x) (quoteWith names y)
quoteWith names (VPartialP x y) = Partial (quoteWith names x) (quoteWith names y)
quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))

refresh :: Set Text -> Text -> Text
refresh s n
  | T.singleton '_' == n = n
  | n `Set.notMember` s = n
  | otherwise = refresh s (n <> T.singleton '\'')

quote :: Value -> Term
quote = quoteWith mempty

data Closure
  = Closure
    { clArgName :: Text
    , clCont    :: Value -> Value
    }

instance Show Closure where
  show (Closure n c) = "Closure \\" ++ show n ++ " -> " ++ show (c (VVar (Bound n)))

instance Eq Closure where
  Closure _ k == Closure _ k' =
    k (VVar (Bound (T.pack "_"))) == k' (VVar (Bound (T.pack "_")))

instance Ord Closure where
  Closure _ k <= Closure _ k' =
    k (VVar (Bound (T.pack "_"))) <= k' (VVar (Bound (T.pack "_")))

data Head
  = HVar Name
  | HMeta MV
  deriving (Eq, Show, Ord)

data Projection
  = PApp   Plicity Value
  | PIElim Value Value Value NFEndp
  | PProj1
  | PProj2
  deriving (Eq, Show, Ord)