quox/lib/Quox/Parser/Syntax.idr
rhiannon morris 0514fff481 represent ℕ constants directly
instead of as huge `succ (succ (succ ⋯))` terms
2023-11-03 18:05:54 +01:00

228 lines
5.1 KiB
Idris

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
| IOState 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
| Nat Nat Loc | Succ PTerm Loc
| STRING Loc -- "String" is a reserved word in idris
| Str String 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
public export %inline
Zero : Loc -> PTerm
Zero = Nat 0
%runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show, PrettyVal]
export
Located PTerm where
(TYPE _ loc).loc = loc
(IOState 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
(Nat _ loc).loc = loc
(Succ _ loc).loc = loc
(STRING loc).loc = loc
(Str _ 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
PFile : Type
PFile = List PTopLevel