diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2025-01-30 16:57:47 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2025-03-13 13:20:29 +0000 |
| commit | f5b75edd91389f0a45045b707abfa36c746e8d54 (patch) | |
| tree | c675419958ad913d111ebda51c5863a752768577 /src/Inky/Term/Parser.idr | |
| parent | 3f4e0844880a43ae113f75711bfcb60b9f22a4dd (diff) | |
Modify definition of data types.
Diffstat (limited to 'src/Inky/Term/Parser.idr')
| -rw-r--r-- | src/Inky/Term/Parser.idr | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index e977bc2..5cfd06b 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -37,6 +37,7 @@ data InkyKind | FoldCase | Fold | By + | Data | Nat | List | Suc @@ -78,6 +79,7 @@ Eq InkyKind where FoldCase == FoldCase = True Fold == Fold = True By == By = True + Data == Data = True Nat == Nat = True List == List = True Suc == Suc = True @@ -120,6 +122,7 @@ Interpolation InkyKind where interpolate FoldCase = "'foldcase'" interpolate Fold = "'fold'" interpolate By = "'by'" + interpolate Data = "'Data'" interpolate Nat = "'Nat'" interpolate List = "'List'" interpolate Suc = "'suc'" @@ -167,6 +170,7 @@ TokenKind InkyKind where tokValue FoldCase = const () tokValue Fold = const () tokValue By = const () + tokValue Data = const () tokValue Nat = const () tokValue List = const () tokValue Suc = const () @@ -204,6 +208,7 @@ keywords = , ("foldcase", FoldCase) , ("fold", Fold) , ("by", By) + , ("data", Data) , ("Nat", Nat) , ("List", List) , ("suc", Suc) @@ -393,17 +398,6 @@ parseList3 (x :: xs) = -- Types ----------------------------------------------------------------------- -OpenOrFixpointType : TypeParser [<] [<"openType"] -OpenOrFixpointType = - OneOf - [ mkFix <$> - Seq [match Backslash, match TypeIdent, match DoubleArrow, Var (%%% "openType")] - , Var (%%% "openType") - ] - where - mkFix : HList [(), String, (), TypeFun] -> TypeFun - mkFix [_, x, _, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x)) - AtomType : TypeParser [<"openType"] [<] AtomType = OneOf @@ -411,7 +405,7 @@ AtomType = , MkParseFun (\_ => Ok TNat) <$ match Nat , mkProd <$> enclose (match AngleOpen) (match AngleClose) row , mkSum <$> enclose (match BracketOpen) (match BracketClose) row - , enclose (match ParenOpen) (match ParenClose) OpenOrFixpointType + , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openType")) ] where row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun) @@ -428,11 +422,19 @@ AppType = OneOf [ AtomType , match List **> mkList <$> weaken (S Z) AtomType + , mkFix <$> Seq + [ match Data + , match TypeIdent + , weaken (S Z) AtomType + ] ] where mkList : TypeFun -> TypeFun mkList x = MkParseFun (\ctx => TList <$> x.try ctx) + mkFix : HList [(), String, TypeFun] -> TypeFun + mkFix [_, x, a] = MkParseFun (\ctx => TFix x <$> a.try (ctx :< x)) + export OpenType : TypeParser [<] [<] OpenType = |