quox/lib/Quox/Definition.idr

module Quox.Definition

import public Quox.No
import public Quox.Syntax
import public Data.SortedMap
import Control.Eff
import Decidable.Decidable


public export
data DefBody =
    Concrete (Term 0 0)
  | Postulate

namespace DefBody
  public export
  (.term0) : DefBody -> Maybe (Term 0 0)
  (Concrete t).term0 = Just t
  (Postulate).term0  = Nothing


public export
record Definition where
  constructor MkDef
  qty   : GQty
  type0 : Term 0 0
  body0 : DefBody

public export %inline
mkPostulate : GQty -> (type0 : Term 0 0) -> Definition
mkPostulate qty type0 = MkDef {qty, type0, body0 = Postulate}

public export %inline
mkDef : GQty -> (type0, term0 : Term 0 0) -> Definition
mkDef qty type0 term0 = MkDef {qty, type0, body0 = Concrete term0}


parameters {d, n : Nat}
  public export %inline
  (.type) : Definition -> Term d n
  g.type = g.type0 // shift0 d // shift0 n

  public export %inline
  (.term) : Definition -> Maybe (Term d n)
  g.term = g.body0.term0 <&> \t => t // shift0 d // shift0 n

  public export %inline
  toElim : Definition -> Maybe $ Elim d n
  toElim def = pure $ !def.term :# def.type


public export %inline
isZero : Definition -> Bool
isZero g = g.qty.fst == Zero


public export
data DefEnvTag = NS | DEFS

public export
Definitions : Type
Definitions = SortedMap Name Definition

public export
0 CurNSReader : Type -> Type
CurNSReader = ReaderL NS Mods

public export
0 DefsReader : Type -> Type
DefsReader = ReaderL DEFS Definitions

export
ns : Has CurNSReader fs => Eff fs Mods
ns = askAt NS

export
defs : Has DefsReader fs => Eff fs Definitions
defs = askAt DEFS


public export
lookupNS : Mods -> Name -> Definitions -> Maybe Definition
lookupNS [<]           x defs = lookup x defs
lookupNS mms@(ms :< _) x defs =
  lookup (addMods mms x) defs <|> lookupNS ms x defs

parameters {d, n : Nat}
  public export %inline
  lookupElim : Name -> Definitions -> Maybe (Elim d n)
  lookupElim x defs = toElim !(lookup x defs)

  public export %inline
  lookupElimNS : Mods -> Name -> Definitions -> Maybe (Elim d n)
  lookupElimNS mods x defs = toElim !(lookupNS mods x defs)