From 0ecd9e608ced18f70f465c986d6519e8e95b0b6b Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 20 Nov 2024 15:31:25 +0000 Subject: Improve syntactic sugar. Sugar makes programs nicer to write. --- src/Inky/Term.idr | 37 -------------- src/Inky/Term/Checks.idr | 1 + src/Inky/Term/Parser.idr | 37 ++++++++++++-- src/Inky/Term/Pretty.idr | 108 ++++++++++++++++++++++++++++------------- src/Inky/Term/Pretty/Error.idr | 3 +- src/Inky/Term/Sugar.idr | 73 ++++++++++++++++++++++++++++ 6 files changed, 183 insertions(+), 76 deletions(-) create mode 100644 src/Inky/Term/Sugar.idr (limited to 'src/Inky') diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 54ac9fe..8fd15aa 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -548,40 +548,3 @@ Uninhabited (NotSynths tyEnv tmEnv (Var meta i)) where uninhabited (ChecksNS Case) impossible uninhabited (ChecksNS Roll) impossible uninhabited (ChecksNS Fold) impossible - --- Sugar ----------------------------------------------------------------------- - -public export -CheckLit : m -> Nat -> Term mode m tyCtx tmCtx -CheckLit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<]) -CheckLit meta (S n) = Roll meta (Inj meta "S" $ CheckLit meta n) - -public export -Lit : m -> Nat -> Term mode m tyCtx tmCtx -Lit meta n = Annot meta (CheckLit meta n) TNat - -public export -Suc : m -> Term mode m tyCtx tmCtx -Suc meta = - Annot meta (Abs meta (["_x"] ** Roll meta (Inj meta "S" $ Var meta (%% "_x")))) - (TArrow TNat TNat) - -export -isCheckLit : Term mode m tyCtx tmCtx -> Maybe Nat -isCheckLit (Roll _ (Inj _ "Z" (Tup _ (MkRow [<] _)))) = Just 0 -isCheckLit (Roll _ (Inj _ "S" t)) = S <$> isCheckLit t -isCheckLit _ = Nothing - -export -isLit : Term mode m tyCtx tmCtx -> Maybe Nat -isLit (Annot _ t a) = - if (alpha {ctx2 = [<]} a TNat).does - then isCheckLit t - else Nothing -isLit _ = Nothing - -export -isSuc : Term mode m tyCtx tmCtx -> Bool -isSuc (Annot _ (Abs _ ([x] ** Roll _ (Inj _ "S" $ Var _ ((%%) x {pos = Here})))) a) = - does (alpha {ctx2 = [<]} a (TArrow TNat TNat)) -isSuc _ = False diff --git a/src/Inky/Term/Checks.idr b/src/Inky/Term/Checks.idr index 402f623..829561a 100644 --- a/src/Inky/Term/Checks.idr +++ b/src/Inky/Term/Checks.idr @@ -204,6 +204,7 @@ fallbackCheck prf p a = (either (EmbedNC1 prf) (\xPrf => uncurry (EmbedNC2 prf) $ snd xPrf)) $ (b := p) >=> alpha b a +export synths : (tyEnv : All (Assoc0 $ Ty [<]) tyCtx) -> (tmEnv : All (Assoc0 $ Ty [<]) tmCtx) -> diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index 6fd4044..1f9d983 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -18,6 +18,7 @@ import Flap.Parser import Inky.Data.Row import Inky.Term +import Inky.Term.Sugar import Inky.Type import Text.Lexer @@ -39,6 +40,7 @@ data InkyKind | Nat | List | Suc + | Cons | Map | ParenOpen | ParenClose @@ -76,6 +78,7 @@ export Nat == Nat = True List == List = True Suc == Suc = True + Cons == Cons = True Map == Map = True ParenOpen == ParenOpen = True ParenClose == ParenClose = True @@ -114,6 +117,7 @@ Interpolation InkyKind where interpolate Nat = "'Nat'" interpolate List = "'List'" interpolate Suc = "'suc'" + interpolate Cons = "'cons'" interpolate Map = "'map'" interpolate ParenOpen = "'('" interpolate ParenClose = "')'" @@ -156,6 +160,7 @@ TokenKind InkyKind where tokValue Nat = const () tokValue List = const () tokValue Suc = const () + tokValue Cons = const () tokValue Map = const () tokValue ParenOpen = const () tokValue ParenClose = const () @@ -190,6 +195,7 @@ keywords = , ("Nat", Nat) , ("List", List) , ("suc", Suc) + , ("cons", Cons) , ("map", Map) ] @@ -386,7 +392,10 @@ AtomTerm = OneOf [ mkVar2 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent) , mkLit <$> WithBounds (match Lit) - , mkSuc <$> WithBounds (match Suc) + , mkList <$> WithBounds ( + enclose (match BracketOpen) (match BracketClose) $ + sepBy (match Comma) $ + Var (%%% "openTerm")) , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $ RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm"))) , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm")) @@ -395,8 +404,13 @@ AtomTerm = mkLit : WithBounds Nat -> TermFun mkLit k = MkParseFun (\tyCtx, tmCtx => pure (Lit k.bounds k.val)) - mkSuc : WithBounds () -> TermFun - mkSuc x = MkParseFun (\_, _ => pure (Suc x.bounds)) + mkList : WithBounds (List TermFun) -> TermFun + mkList xs = + MkParseFun (\tyCtx, tmCtx => + foldr + (\x, ys => pure $ Cons xs.bounds !(x.try tyCtx tmCtx) !ys) + (pure $ Nil xs.bounds) + xs.val) mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun mkTup xs = MkParseFun (\tyCtx, tmCtx => Tup xs.bounds <$> tryRow2 xs.val tyCtx tmCtx) @@ -431,6 +445,15 @@ AppTerm = [ WithBounds (match TypeIdent) , weaken (S Z) SuffixTerm ] + , mkSuc <$> Seq + [ WithBounds (match Suc) + , weaken (S Z) SuffixTerm + ] + , mkCons <$> Seq + [ WithBounds (match Cons) + , weaken (S Z) SuffixTerm + , weaken (S Z) SuffixTerm + ] , mkApp <$> Seq [ OneOf [ WithBounds SuffixTerm @@ -453,6 +476,14 @@ AppTerm = mkInj : HList [WithBounds String, TermFun] -> TermFun mkInj [tag, t] = MkParseFun (\tyCtx, tmCtx => Inj tag.bounds tag.val <$> t.try tyCtx tmCtx) + mkSuc : HList [WithBounds _, TermFun] -> TermFun + mkSuc [x, t] = MkParseFun (\tyCtx, tmCtx => Suc x.bounds <$> t.try tyCtx tmCtx) + + mkCons : HList [WithBounds _, TermFun, TermFun] -> TermFun + mkCons [x, t, u] = + MkParseFun (\tyCtx, tmCtx => + pure $ Cons x.bounds !(t.try tyCtx tmCtx) !(u.try tyCtx tmCtx)) + mkMap : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun, TypeFun] -> WithBounds TermFun mkMap [m, [_, x, _, a], b, c] = MkParseFun (\tyCtx, tmCtx => diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr index a4bb1e1..0523362 100644 --- a/src/Inky/Term/Pretty.idr +++ b/src/Inky/Term/Pretty.idr @@ -5,6 +5,7 @@ import Data.String import Inky.Term import Inky.Type.Pretty +import Inky.Term.Sugar import Text.Bounded import Text.PrettyPrint.Prettyprinter @@ -46,26 +47,53 @@ Ord TermPrec where export prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term mode m tyCtx tmCtx) -> TermPrec -> List (Doc ann) -prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann) +prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term mode m tyCtx tmCtx) -> SnocList (Doc ann) prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term mode m tyCtx (tmCtx :< x)) -> SnocList (Doc ann) -prettyLet : Doc ann -> Doc ann -> Doc ann +prettyLet : + (eqLine : Doc ann) -> + (doc : List String) -> + (bound, body : Doc ann) -> + Doc ann lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term mode m tyCtx tmCtx -> TermPrec -> Doc ann prettyTerm t d = - case isLit t <|> isCheckLit t of + case isLit t of Just k => pretty k Nothing => - if isSuc t - then pretty "suc" - else lessPrettyTerm t d + case isSuc t of + Just u => + group $ align $ hang 2 $ parenthesise (d < App) $ + concatWith (surround line) [pretty "suc", prettyTerm (assert_smaller t u) Suffix] + Nothing => case isList t of + Just ts => + let ts = prettyAllTerm (assert_smaller t ts) Open in + group $ align $ flatAlt + (enclose ("[" <++> neutral) (line <+> "]") $ + concatWith (surround $ line <+> "," <++> neutral) ts) + (enclose "[" "]" $ concatWith (surround $ "," <++> neutral) ts) + Nothing => case isCons t of + Just (hd, tl) => + group $ align $ hang 2 $ parenthesise (d < App) $ + concatWith (surround line) + [ pretty "cons" + , prettyTerm (assert_smaller t hd) Suffix + , prettyTerm (assert_smaller t tl) Suffix + ] + Nothing => lessPrettyTerm t d prettyAllTerm [] d = [] prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d -prettyTermCtx [<] d = [<] -prettyTermCtx (ts :< (l :- t)) d = - prettyTermCtx ts d :< - (group $ hang 2 $ pretty l <+> ":" <+> line <+> prettyTerm t d) +prettyTermCtx [<] = [<] +prettyTermCtx (ts :< (l :- Abs _ (bound ** t))) = + prettyTermCtx ts :< + (group $ align $ + pretty l <+> ":" <++> + "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+> + prettyTerm t Open) +prettyTermCtx (ts :< (l :- t)) = + prettyTermCtx ts :< + (group $ align $ pretty l <+> ":" <+> line <+> prettyTerm t Open) prettyCases [<] = [<] prettyCases (ts :< (l :- (x ** Abs _ (bound ** t)))) = @@ -80,12 +108,21 @@ prettyCases (ts :< (l :- (x ** t))) = pretty l <++> pretty x <++> "=>" <+> line <+> prettyTerm t Open) -prettyLet binding term = +prettyLet eqLine [] bound body = + group $ (group $ - pretty "let" <++> - (group $ hang (-2) $ binding) <+> line <+> + hang 2 + (group (pretty "let" <++> eqLine) <+> line <+> + group bound) <+> line <+> "in") <+> line <+> - term + group body +prettyLet eqLine doc bound body = + (hang 2 $ + group (pretty "let" <++> eqLine) <+> hardline <+> + concatMap (enclose "--" hardline . pretty) doc <+> + group bound) <+> hardline <+> + "in" <+> line <+> + group body lessPrettyTerm (Annot _ t a) d = group $ align $ parenthesise (d < Annot) $ @@ -95,22 +132,22 @@ lessPrettyTerm (Var _ i) d = pretty (unVal $ nameOf i) lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d = let (binds, cod, rest) = groupBinds bound a in let binds = map (\x => parens (pretty x.name <++> ":" <++> prettyType x.value Open)) binds in - let doc = concatMap (enclose "--" hardline . pretty) meta.doc in group $ align $ parenthesise (d < Open) $ prettyLet - ( (group $ hang 2 $ flatAlt + (group $ hang 2 $ flatAlt ( pretty x <+> line <+> concatWith (surround line) binds <+> line <+> - ":" <++> prettyType cod Open + ":" <++> prettyType cod Open <++> "=" <+> + if null rest then neutral + else line <+> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>" ) - (pretty x <++> concatWith (<++>) binds <++> ":" <++> prettyType cod Open) - ) <++> "=" <+> - ( if null rest - then neutral - else neutral <++> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>") - <+> line <+> doc <+> prettyTerm e Open - ) - (prettyTerm t Open) + ( pretty x <++> concatWith (<++>) binds <++> ":" <++> prettyType cod Open <++> "=" <+> + if null rest then neutral + else neutral <++> "\\" <+> concatWith (surround $ "," <++> neutral) (map pretty rest) <++> "=>" + )) + meta.doc + (prettyTerm e Open) + (prettyTerm t Open) where groupBinds : List String -> Ty tyCtx -> (List (Assoc $ Ty tyCtx), Ty tyCtx, List String) groupBinds [] a = ([], a, []) @@ -119,24 +156,25 @@ lessPrettyTerm (Let meta (Annot _ (Abs _ (bound ** e)) a) (x ** t)) d = ((x :- a) :: binds, cod, rest) groupBinds xs a = ([], a, xs) lessPrettyTerm (Let meta (Annot _ e a) (x ** t)) d = - let doc = concatMap (enclose "--" hardline . pretty) meta.doc in group $ align $ parenthesise (d < Open) $ prettyLet - ( pretty x <++> ":" <++> prettyType a Open <++> "=" <+> line <+> - doc <+> prettyTerm e Open - ) + (pretty x <+> line <+> ":" <++> prettyType a Open <++> "=") + meta.doc + (prettyTerm e Open) (prettyTerm t Open) lessPrettyTerm (Let meta e (x ** t)) d = - let doc = concatMap (enclose "--" hardline . pretty) meta.doc in group $ align $ parenthesise (d < Open) $ prettyLet - (pretty x <++> "=" <+> line <+> doc <+> prettyTerm e Open) + (pretty x <++> "=") + meta.doc + (prettyTerm e Open) (prettyTerm t Open) lessPrettyTerm (LetTy meta a (x ** t)) d = - let doc = concatMap (enclose "--" hardline . pretty) meta.doc in group $ align $ parenthesise (d < Open) $ prettyLet - (pretty x <++> "=" <+> line <+> doc <+> prettyType a Open) + (pretty x <++> "=") + meta.doc + (prettyType a Open) (prettyTerm t Open) lessPrettyTerm (Abs _ (bound ** t)) d = group $ hang 2 $ parenthesise (d < Open) $ @@ -154,7 +192,7 @@ lessPrettyTerm (App _ f ts) d = group $ align $ hang 2 $ parenthesise (d < App) $ concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix) lessPrettyTerm (Tup _ (MkRow ts _)) d = - let parts = prettyTermCtx ts Open <>> [] in + let parts = prettyTermCtx ts <>> [] in group $ align $ enclose "<" ">" $ flatAlt (neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line) @@ -168,7 +206,7 @@ lessPrettyTerm (Inj _ l t) d = lessPrettyTerm (Case _ e (MkRow ts _)) d = let parts = prettyCases ts <>> [] in group $ align $ hang 2 $ parenthesise (d < Open) $ - (group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+> + (group $ "case" <++> prettyTerm e Open <++> "of") <+> line <+> (braces $ flatAlt (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line) (concatWith (surround $ ";" <++> neutral) parts)) diff --git a/src/Inky/Term/Pretty/Error.idr b/src/Inky/Term/Pretty/Error.idr index a5ee2fa..d87178f 100644 --- a/src/Inky/Term/Pretty/Error.idr +++ b/src/Inky/Term/Pretty/Error.idr @@ -22,6 +22,7 @@ Pretty (ChecksOnly t) where pretty Roll = "rolling" pretty Fold = "fold" +export prettyNotSynths : {tyCtx, tmCtx : SnocList String} -> {e : Term mode m tyCtx tmCtx} -> @@ -99,7 +100,7 @@ prettyNotSynths (PrjNS2 prf f) = , pretty "cannot project non-product type" <+> line <+> prettyType a Open )] -prettyNotSynths (PrjNS3 {l, as} prf contra) = +prettyNotSynths (PrjNS3 {l, e, as} prf contra) = case synthsRecompute prf of Val (TProd as) => [(e.meta diff --git a/src/Inky/Term/Sugar.idr b/src/Inky/Term/Sugar.idr new file mode 100644 index 0000000..477df5e --- /dev/null +++ b/src/Inky/Term/Sugar.idr @@ -0,0 +1,73 @@ +module Inky.Term.Sugar + +import Flap.Decidable +import Inky.Term + +-- Naturals -------------------------------------------------------------------- + +export +Zero : m -> Term mode m tyCtx tmCtx +Zero meta = Roll meta (Inj meta "Z" $ Tup meta [<]) + +export +Suc : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx +Suc meta t = Roll meta (Inj meta "S" t) + +export +isZero : Term mode m tyCtx tmCtx -> Bool +isZero (Roll _ (Inj _ "Z" $ Tup _ $ MkRow [<] _)) = True +isZero _ = False + +export +isSuc : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx) +isSuc (Roll _ (Inj _ "S" t)) = Just t +isSuc _ = Nothing + +export +Lit : m -> Nat -> Term mode m tyCtx tmCtx +Lit meta 0 = Roll meta (Inj meta "Z" $ Tup meta [<]) +Lit meta (S n) = Suc meta (Lit meta n) + +export +isLit : Term mode m tyCtx tmCtx -> Maybe Nat +isLit t = + if isZero t then Just 0 + else do + u <- isSuc t + k <- isLit (assert_smaller t u) + pure (S k) + +-- Lists ----------------------------------------------------------------------- + +export +Nil : m -> Term mode m tyCtx tmCtx +Nil meta = Roll meta (Inj meta "N" $ Tup meta [<]) + +export +Cons : m -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx -> Term mode m tyCtx tmCtx +Cons meta t ts = Roll meta (Inj meta "C" $ Tup meta [<"H" :- t, "T" :- ts]) + +export +fromList : m -> List (Term mode m tyCtx tmCtx) -> Term mode m tyCtx tmCtx +fromList meta [] = Nil meta +fromList meta (t :: ts) = Cons meta t (fromList meta ts) + +export +isNil : Term mode m tyCtx tmCtx -> Bool +isNil (Roll _ (Inj _ "N" $ Tup _ $ MkRow [<] _)) = True +isNil _ = False + +export +isCons : Term mode m tyCtx tmCtx -> Maybe (Term mode m tyCtx tmCtx, Term mode m tyCtx tmCtx) +isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"H" :- t, "T" :- ts] _)) = Just (t, ts) +isCons (Roll _ (Inj _ "C" $ Tup meta $ MkRow [<"T" :- ts, "H" :- t] _)) = Just (t, ts) +isCons _ = Nothing + +export +isList : Term mode m tyCtx tmCtx -> Maybe (List $ Term mode m tyCtx tmCtx) +isList t = + if isNil t then Just [] + else do + (hd, tl) <- isCons t + tl <- isList (assert_smaller t tl) + pure (hd :: tl) -- cgit v1.2.3