module Obs.Typing.Conversion

import Data.Fin

import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
import Obs.Sort
import Obs.Substitution

-- Conversion ------------------------------------------------------------------

-- invariant: all definitions fully expanded
-- invariant: m |- t, u <- a : s
partial export
convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
partial
convertSet : (t, u : NormalForm n) -> Logging ann Bool
partial
convertSum : (t, u : NormalForm n) -> (s, s' : Sort) -> (a, b : NormalForm n) -> Logging ann Bool

-- In sort Prop
convert Irrel Irrel a Prop = pure True
-- In unknown type in set
convert t u (Ntrl _) (Set k) = pure $ t == u
-- In type Set
convert t u (Cnstr (Sort _)) (Set _) = convertSet t u
-- In type Pi
convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
  t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
  u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
  convert t u b s'
-- In type Sigma
convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
  t1 <- doFst t
  u1 <- doFst t
  True <- convert t1 u1 a s
    | False => pure False
  b <- subst1 t1 b
  t2 <- doSnd t
  u2 <- doSnd t
  convert t2 u2 b s'
-- In type Sum (manually expanding definition of doCase)
convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b
-- Default
convert t u a s =
  inScope "invalid conversion" $ fatal $
  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]

convertSet (Cnstr (Sort s')) (Cnstr (Sort s'')) = pure $ s' == s''
convertSet (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) =
  pure $
  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) =
  pure $
  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) =
  pure $
  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
convertSet (Cnstr Top) (Cnstr Top) = pure True
convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True
convertSet (Ntrl t) u = pure (Ntrl t == u)
convertSet t (Ntrl u) = pure (t == Ntrl u)
convertSet t u = pure $ False

convertSum (Cnstr (Left t)) (Cnstr (Left u)) s s' a b = convert t u a s
convertSum (Cnstr (Right t)) (Cnstr (Right u)) s s' a b = convert t u b s'
convertSum (Ntrl t) u s s' a b = pure (Ntrl t == u)
convertSum t (Ntrl u) s s' a b = pure (t == Ntrl u)
convertSum t u s s' a b = pure False