diff options
| -rw-r--r-- | program/reducer.prim | 4 | ||||
| -rw-r--r-- | program/reducer.pty | 8 | ||||
| -rw-r--r-- | src/Inky.idr | 2 | ||||
| -rw-r--r-- | src/Inky/Term/Parser.idr | 26 | ||||
| -rw-r--r-- | src/Inky/Type/Pretty.idr | 5 |
5 files changed, 23 insertions, 22 deletions
diff --git a/program/reducer.prim b/program/reducer.prim index 3abbc97..af3abd5 100644 --- a/program/reducer.prim +++ b/program/reducer.prim @@ -1,14 +1,14 @@ let Bool = [T: <>; F: <>] in let or (x : Bool) (y : Bool) : Bool = case x of {T u => T <>; F u => y} in let SysT = - (\T => + data T [ Var: Nat ; Zero: <> ; Suc: T ; Primrec: <Zero: T; Suc: T; Target: T> ; Abs: T ; App: <Fun: T; Arg: T> - ]) + ] in let Stepped = <Term: SysT; Smaller: Bool> in let lift (f : Nat -> Nat) (n : Nat) : Nat = diff --git a/program/reducer.pty b/program/reducer.pty index c72b8c6..65090e5 100644 --- a/program/reducer.pty +++ b/program/reducer.pty @@ -1,17 +1,17 @@ Nat -> -(\T => +data T [ Var: Nat ; Zero: <> ; Suc: T ; Primrec: <Zero: T; Suc: T; Target: T> ; Abs: T ; App: <Fun: T; Arg: T> - ]) -> -(\T => + ] -> +data T [ Var: Nat ; Zero: <> ; Suc: T ; Primrec: <Zero: T; Suc: T; Target: T> ; Abs: T ; App: <Fun: T; Arg: T> - ]) + ] diff --git a/src/Inky.idr b/src/Inky.idr index 3f6b755..7fa9cad 100644 --- a/src/Inky.idr +++ b/src/Inky.idr @@ -76,7 +76,7 @@ readFileOrStdin (Just path) = withFile path Read throw readFile lexInkyString : HasErr (WithBounds String) es => String -> App es (List (WithBounds InkyToken)) lexInkyString file = do let (tokens, _, _, "") = lex tokenMap file - | (_, line, col, rest) => + | (_, line, col, rest) => throw (MkBounded "unexpected character" False (MkBounds line col line col)) pure (filter (\x => relevant x.val.kind) tokens) 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 = diff --git a/src/Inky/Type/Pretty.idr b/src/Inky/Type/Pretty.idr index 03b9964..7cd185c 100644 --- a/src/Inky/Type/Pretty.idr +++ b/src/Inky/Type/Pretty.idr @@ -78,9 +78,8 @@ lessPrettyType (TSum (MkRow as _)) d = (neutral <++> concatWith (surround $ line <+> ";" <++> neutral) parts <+> line) (concatWith (surround $ ";" <++> neutral) parts) lessPrettyType (TFix x a) d = - group $ align $ hang 2 $ parens $ - "\\" <+> pretty x <++> "=>" <+> line <+> - prettyType a Open + group $ align $ hang 2 $ parenthesise (d < App) $ + pretty "data" <++> pretty x <+> line <+> prettyType a Atom lessPrettyTypeCtx [<] d = [<] lessPrettyTypeCtx (as :< (x :- a)) d = |