module AstExtra

import Quox.Syntax
import Quox.Parser.Syntax
import Quox.Typing.Context

prefix 9 ^
public export
(^) : (Loc -> a) -> a
(^) a = a noLoc

public export
FromString BindName where fromString str = BN (fromString str) noLoc

public export
FromString PatVar where fromString x = PV x noLoc

public export
empty01 : TyContext 0 0
empty01 = eqDim (^K Zero) (^K One) empty


anys : {n : Nat} -> QContext n
anys {n = 0}   = [<]
anys {n = S n} = anys :< Any

public export
locals : Context (Term d) n -> Context (LocalVar d) n
locals = map $ \t => MkLocal t Nothing

public export
ctx, ctx01 : {n : Nat} -> Context (\n => (BindName, Term 0 n)) n ->
             TyContext 0 n
ctx tel = let (ns, ts) = unzip tel in
          MkTyContext new [<] (locals ts) ns anys
ctx01 tel = let (ns, ts) = unzip tel in
            MkTyContext ZeroIsOne [<] (locals ts) ns anys

export
mkDef : GQty -> Term 0 0 -> Term 0 0 -> Definition
mkDef q ty tm = Definition.mkDef q ty tm Nothing False noLoc
%hide Definition.mkDef

export
mkPostulate : GQty -> Term 0 0 -> Definition
mkPostulate q ty = Definition.mkPostulate q ty Nothing False noLoc
%hide Definition.mkPostulate