quox/lib/Quox/Parser/Syntax.idr

module Quox.Parser.Syntax

import public Quox.Loc
import public Quox.Syntax
import public Quox.Definition
import Quox.PrettyValExtra

import Derive.Prelude
%hide TT.Name

%default total
%language ElabReflection


public export
data PatVar = Unused Loc | PV PBaseName Loc
%name PatVar v
%runElab derive "PatVar" [Eq, Ord, Show, PrettyVal]

export
Located PatVar where
  (Unused loc).loc = loc
  (PV _   loc).loc = loc

export
(.name) : PatVar -> Maybe PBaseName
(Unused _).name = Nothing
(PV nm  _).name = Just nm

export
isUnused : PatVar -> Bool
isUnused (Unused {}) = True
isUnused _           = False


public export
record PQty where
  constructor PQ
  val  : Qty
  loc_ : Loc
%name PQty qty
%runElab derive "PQty" [Eq, Ord, Show, PrettyVal]

export Located PQty where q.loc = q.loc_

namespace PDim
  public export
  data PDim = K DimConst Loc | V PBaseName Loc
  %name PDim p, q
  %runElab derive "PDim" [Eq, Ord, Show, PrettyVal]

export
Located PDim where
  (K _ loc).loc = loc
  (V _ loc).loc = loc

public export
data PTagVal = PT TagVal Loc
%name PTagVal tag
%runElab derive "PTagVal" [Eq, Ord, Show, PrettyVal]


namespace PTerm
  mutual
    ||| terms out of the parser with BVs and bidirectionality still tangled up
    public export
    data PTerm =
        TYPE Universe Loc

      | Pi PQty PatVar PTerm PTerm Loc
      | Lam PatVar PTerm Loc
      | App PTerm PTerm Loc

      | Sig PatVar PTerm PTerm Loc
      | Pair PTerm PTerm Loc
      | Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
      | Fst PTerm Loc | Snd PTerm Loc

      | Enum (List TagVal) Loc
      | Tag TagVal Loc

      | Eq (PatVar, PTerm) PTerm PTerm Loc
      | DLam PatVar PTerm Loc
      | DApp PTerm PDim Loc

      | Nat Loc
      | Zero Loc | Succ PTerm Loc

      | BOX PQty PTerm Loc
      | Box PTerm Loc

      | V PName (Maybe Universe) Loc
      | Ann PTerm PTerm Loc

      | Coe (PatVar, PTerm) PDim PDim PTerm Loc
      | Comp (PatVar, PTerm) PDim PDim PTerm PDim
             (PatVar, PTerm) (PatVar, PTerm) Loc
    %name PTerm s, t

    public export
    data PCaseBody =
        CasePair (PatVar, PatVar) PTerm Loc
      | CaseEnum (List (PTagVal, PTerm)) Loc
      | CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc
      | CaseBox PatVar PTerm Loc
    %name PCaseBody body

%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show, PrettyVal]

export
Located PTerm where
  (TYPE _             loc).loc = loc
  (Pi   _ _ _ _       loc).loc = loc
  (Lam  _ _           loc).loc = loc
  (App  _ _           loc).loc = loc
  (Sig  _ _ _         loc).loc = loc
  (Pair _ _           loc).loc = loc
  (Fst  _             loc).loc = loc
  (Snd  _             loc).loc = loc
  (Case _ _ _ _       loc).loc = loc
  (Enum _             loc).loc = loc
  (Tag  _             loc).loc = loc
  (Eq   _ _ _         loc).loc = loc
  (DLam _ _           loc).loc = loc
  (DApp _ _           loc).loc = loc
  (Nat                loc).loc = loc
  (Zero               loc).loc = loc
  (Succ _             loc).loc = loc
  (BOX  _ _           loc).loc = loc
  (Box  _             loc).loc = loc
  (V    _ _           loc).loc = loc
  (Ann  _ _           loc).loc = loc
  (Coe  _ _ _ _       loc).loc = loc
  (Comp _ _ _ _ _ _ _ loc).loc = loc

export
Located PCaseBody where
  (CasePair _ _ loc).loc = loc
  (CaseEnum _   loc).loc = loc
  (CaseNat  _ _ loc).loc = loc
  (CaseBox  _ _ loc).loc = loc


public export
data PBody = PConcrete (Maybe PTerm) PTerm | PPostulate PTerm
%name PBody body
%runElab derive "PBody" [Eq, Ord, Show, PrettyVal]


public export
record PDefinition where
  constructor MkPDef
  qty  : PQty
  name : PBaseName
  body : PBody
  loc_ : Loc
%name PDefinition def
%runElab derive "PDefinition" [Eq, Ord, Show, PrettyVal]

export Located PDefinition where def.loc = def.loc_

public export
data PDeclMod =
    PFail (Maybe String)
  | PCompileScheme String
  | PMain
%name PDeclMod mod
%runElab derive "PDeclMod" [Eq, Ord, Show, PrettyVal]

mutual
  public export
  record PNamespace where
    constructor MkPNamespace
    name  : Mods
    decls : List PDecl
    loc_  : Loc
  %name PNamespace ns

  public export
  record PDecl where
    constructor MkPDecl
    mods : List PDeclMod
    decl : PDeclBody
    loc_ : Loc

  public export
  data PDeclBody =
      PDef  PDefinition
    | PNs   PNamespace
  %name PDeclBody decl
%runElab deriveMutual ["PNamespace", "PDecl", "PDeclBody"]
                      [Eq, Ord, Show, PrettyVal]

export Located PNamespace where ns.loc = ns.loc_

export Located PDecl where decl.loc = decl.loc_

export
Located PDeclBody where
  (PDef  def).loc  = def.loc
  (PNs   ns).loc   = ns.loc

public export
data PTopLevel = PD PDecl | PLoad String Loc
%name PTopLevel t
%runElab derive "PTopLevel" [Eq, Ord, Show, PrettyVal]

export
Located PTopLevel where
  (PD    decl).loc  = decl.loc
  (PLoad _ loc).loc = loc


public export
fromNat : Nat -> Loc -> PTerm
fromNat 0     loc = Zero loc
fromNat (S k) loc = Succ (fromNat k loc) loc


public export
PFile : Type
PFile = List PTopLevel