module Obs.Abstract

import Data.Fin
import Data.String

import Obs.Syntax
import Obs.Term

import System
import Text.Bounded

%default total

public export
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

Error : Type -> Type
Error = Either (Bounds, String)

report : Bounds -> String -> Error a
report = curry Left

export
printErr : Error a -> IO a
printErr (Left (b, str)) = do
  () <- putStrLn "error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
  exitFailure
printErr (Right x) = pure x

export
abstractSyntax : Context n -> Syntax -> Error (Term n)
abstractSyntax ctx (Var b str) = do
  let Just i = lookup str ctx
    | Nothing => report b "unbound variable: \{str}"
  pure (Var b i)
abstractSyntax ctx (Sort b s) = pure (Sort b s)
abstractSyntax ctx (Top b) = pure (Top b)
abstractSyntax ctx (Point b) = pure (Point b)
abstractSyntax ctx (Bottom b) = pure (Bottom b)
abstractSyntax ctx (Absurd b a t) = do
  a <- abstractSyntax ctx a
  t <- abstractSyntax ctx t
  pure (Absurd b a t)

export
abstractDefinition : Context n -> Definition -> Error (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) -> Error (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) -> Error (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