module Obs.Abstract

import Data.Fin
import Data.String

import Obs.Logging
import Obs.Syntax
import Obs.Term

import System
import Text.Bounded

%default total

Context : Nat -> Type
Context n = List (String, Fin n)

bind : Context n -> String -> Context (S n)
bind ctx str = (str, 0) :: map (mapSnd FS) ctx

abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))

abstractSyntax ctx (Var var) = do
  let Just i = lookup var ctx
    | Nothing => inScope "unbound variable" $ fatal var
  pure (Var var i)
abstractSyntax ctx (Sort s) = pure (Sort s)
abstractSyntax ctx (Pi var a b) = do
  a <- abstractSyntaxBounds ctx a
  b <- abstractSyntaxBounds (bind ctx var.val) b
  pure (Pi var a b)
abstractSyntax ctx (Lambda var t) = do
  t <- abstractSyntaxBounds (bind ctx var.val) t
  pure (Lambda var t)
abstractSyntax ctx (App t u) = do
  t <- abstractSyntaxBounds ctx t
  u <- abstractSyntaxBounds ctx u
  pure (App t u)
abstractSyntax ctx (Sigma var a b) = do
  a <- abstractSyntaxBounds ctx a
  b <- abstractSyntaxBounds (bind ctx var.val) b
  pure (Sigma var a b)
abstractSyntax ctx (Pair t u) = do
  t <- abstractSyntaxBounds ctx t
  u <- abstractSyntaxBounds ctx u
  pure (Pair t u)
abstractSyntax ctx (Fst t) = do
  t <- abstractSyntaxBounds ctx t
  pure (Fst t)
abstractSyntax ctx (Snd t) = do
  t <- abstractSyntaxBounds ctx t
  pure (Snd t)
abstractSyntax ctx Top = pure Top
abstractSyntax ctx Point = pure Point
abstractSyntax ctx Bottom = pure Bottom
abstractSyntax ctx (Absurd a t) = do
  a <- abstractSyntaxBounds ctx a
  t <- abstractSyntaxBounds ctx t
  pure (Absurd a t)
abstractSyntax ctx (Equal t u) = do
  t <- abstractSyntaxBounds ctx t
  u <- abstractSyntaxBounds ctx u
  pure (Equal t u)
abstractSyntax ctx (Refl t) = do
  t <- abstractSyntaxBounds ctx t
  pure (Refl t)
abstractSyntax ctx (Transp t b u t' e) = do
  t <- abstractSyntaxBounds ctx t
  b <- abstractSyntaxBounds ctx b
  u <- abstractSyntaxBounds ctx u
  t' <- abstractSyntaxBounds ctx t'
  e <- abstractSyntaxBounds ctx e
  pure (Transp t b u t' e)
abstractSyntax ctx (Cast b e t) = do
  b <- abstractSyntaxBounds ctx b
  e <- abstractSyntaxBounds ctx e
  t <- abstractSyntaxBounds ctx t
  pure (Cast b e t)
abstractSyntax ctx (CastId t) = do
  t <- abstractSyntaxBounds ctx t
  pure (CastId t)

abstractSyntaxBounds ctx (MkBounded v irrel bnds) =
  pure $ MkBounded !(abstractSyntax ctx v) irrel bnds

abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
abstractDefinition ctx def = pure $ MkDefinition
  { name = def.name
  , ty = !(abstractSyntaxBounds ctx def.ty)
  , tm = !(abstractSyntaxBounds ctx def.tm)
  }

export
abstractBlock : (defs : List Definition) -> Logging ann (Block (length defs))
abstractBlock defs =
  let asContext : Block n -> Context n
      asContext []            = []
      asContext (defs :< def) = bind (asContext defs) def.name.val
  in let helper : Block n -> (defs : List Definition) -> Logging ann (Block (length defs + n))
         helper blk []            = pure blk
         helper blk (def :: defs) = do
           def <- abstractDefinition (asContext blk) def
           (rewrite plusSuccRightSucc (length defs) n in helper (blk :< def) defs)
  in rewrite sym $ plusZeroRightNeutral (length defs) in helper [] defs