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 (Universe {s}) = pure (Universe s) abstractSyntax ctx (Pi {var, domain, codomain}) = do a <- abstractSyntaxBounds ctx domain b <- abstractSyntaxBounds (bind ctx var.val) codomain pure (Pi var a b) abstractSyntax ctx (Lambda {var, body}) = do t <- abstractSyntaxBounds (bind ctx var.val) body pure (Lambda var t) abstractSyntax ctx (App {fun, arg}) = do t <- abstractSyntaxBounds ctx fun u <- abstractSyntaxBounds ctx arg pure (App t u) abstractSyntax ctx (Sigma {var, index, element}) = do a <- abstractSyntaxBounds ctx index b <- abstractSyntaxBounds (bind ctx var.val) element pure (Sigma var a b) abstractSyntax ctx (Pair {first, second}) = do t <- abstractSyntaxBounds ctx first u <- abstractSyntaxBounds ctx second pure (Pair t u) abstractSyntax ctx (First {arg}) = do t <- abstractSyntaxBounds ctx arg pure (Fst t) abstractSyntax ctx (Second {arg}) = do t <- abstractSyntaxBounds ctx arg pure (Snd t) abstractSyntax ctx Bool = pure Bool abstractSyntax ctx True = pure True abstractSyntax ctx False = pure False abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do a <- abstractSyntaxBounds (bind ctx var.val) returnType t <- abstractSyntaxBounds ctx discriminant f <- abstractSyntaxBounds ctx true g <- abstractSyntaxBounds ctx false pure (If var a t f g) abstractSyntax ctx Top = pure Top abstractSyntax ctx Point = pure Point abstractSyntax ctx Bottom = pure Bottom abstractSyntax ctx (Absurd {contradiction}) = do t <- abstractSyntaxBounds ctx contradiction pure (Absurd t) abstractSyntax ctx (Equal {left, right}) = do t <- abstractSyntaxBounds ctx left u <- abstractSyntaxBounds ctx right pure (Equal t u) abstractSyntax ctx (Refl {value}) = do t <- abstractSyntaxBounds ctx value pure (Refl t) abstractSyntax ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do a <- abstractSyntaxBounds ctx indexedType t <- abstractSyntaxBounds ctx oldIndex u <- abstractSyntaxBounds ctx value t' <- abstractSyntaxBounds ctx newIndex e <- abstractSyntaxBounds ctx equality pure (Transp a t u t' e) abstractSyntax ctx (Cast {oldType, newType, equality, value}) = do a <- abstractSyntaxBounds ctx oldType b <- abstractSyntaxBounds ctx newType e <- abstractSyntaxBounds ctx equality t <- abstractSyntaxBounds ctx value pure (Cast a b e t) abstractSyntax ctx (CastId {value}) = do t <- abstractSyntaxBounds ctx value 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