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

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

abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
abstractDefinition ctx def = pure $ MkDefinition
  { name = def.name
  , bounds = def.bounds
  , ty = !(abstractSyntax ctx def.ty)
  , tm = !(abstractSyntax 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
  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