diff options
| -rw-r--r-- | inky.ipkg | 1 | ||||
| -rw-r--r-- | src/Inky.idr | 84 | ||||
| -rw-r--r-- | src/Inky/Term.idr | 5 | ||||
| -rw-r--r-- | src/Inky/Term/Desugar.idr | 12 | ||||
| -rw-r--r-- | src/Inky/Term/Parser.idr | 913 | ||||
| -rw-r--r-- | src/Inky/Term/Pretty.idr | 15 | ||||
| -rw-r--r-- | src/Inky/Term/Rename.idr | 85 |
7 files changed, 508 insertions, 607 deletions
@@ -22,6 +22,7 @@ modules , Inky.Term.Pretty , Inky.Term.Pretty.Error , Inky.Term.Recompute + , Inky.Term.Rename , Inky.Type , Inky.Type.Pretty , Inky.Type.Substitution diff --git a/src/Inky.idr b/src/Inky.idr index 7fa9cad..bf8f26f 100644 --- a/src/Inky.idr +++ b/src/Inky.idr @@ -80,49 +80,51 @@ lexInkyString file = do throw (MkBounded "unexpected character" False (MkBounds line col line col)) pure (filter (\x => relevant x.val.kind) tokens) -Interpolation (List InkyKind) where - interpolate [t] = interpolate t - interpolate ts = "one of " ++ joinBy ", " (map interpolate ts) +ParseErr : Type +ParseErr = ParseErr (WithBounds InkyError) InkyKind doParse : - HasErr (WithBounds String) es => + (e : HasErr (List1 ParseErr) es) => (p : InkyParser False [<] [<] a) -> - {auto 0 wf : collectTypeErrs @{ListSet} [<] [<] [<] [<] p = []} -> + {auto 0 wf : WellFormed ListSet p} -> List (WithBounds InkyToken) -> - App es a -doParse p toks = - case parse @{ListSet} p toks of + (s : state) -> + App es (a s) +doParse p toks s = + case (parse ListSet p).runParser s toks of Ok res [] _ => pure res - Ok res (x :: _) _ => - throw ("expected end of input; got token \{x.val.kind}" <$ x) - Err err => throw (parseErrToString err) - where - parseErrToString : ParseErr InkyKind -> WithBounds String - parseErrToString (BadEOF ts) = - irrelevantBounds "expected \{ts}; got end of input" - parseErrToString (Unexpected ts got) = - "expected \{ts}; got token \{got.val.kind}" <$ got + Ok res (x :: _) _ => throw @{e} (Unexpected [] x ::: []) + SoftErr errs _ _ => throw errs + Err errs => throw errs parseType : - Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es => + Has + [ HasErr (WithBounds String) + , HasErr (List1 ParseErr) + , HasErr Err + , HasErr IOError + , FileIO + ] es => Maybe FilePath -> App es (Ty [<]) parseType path = do txt <- readFileOrStdin path toks <- lexInkyString txt - res <- doParse OpenType toks - let Ok a = res.try [<] - | Errs errs => throw errs - pure a + doParse OpenType toks [<] parseTerm : - Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es => - (termPath, tyPath : Maybe FilePath) -> App es (Term (Sugar [<]) Bounds [<] [<]) + Has + [ HasErr (WithBounds String) + , HasErr (List1 ParseErr) + , HasErr Err + , HasErr IOError + , FileIO + ] es => + (termPath, tyPath : Maybe FilePath) -> + App es (Term (Sugar [<]) Bounds [<] [<]) parseTerm termPath tyPath = do txt <- readFileOrStdin termPath toks <- lexInkyString txt - res <- doParse OpenTerm toks - let Ok t = res.try (Sugar [<]) [<] [<] - | Errs errs => throw errs + t <- doParse OpenTerm toks (Sugar [<], [<], [<]) -- Annotate with type let Just _ = tyPath | Nothing => pure t @@ -237,6 +239,7 @@ process : [ HasErr String , HasErr (WithBounds String) , HasErr (List1 $ WithBounds String) + , HasErr (List1 $ ParseErr) , HasErr (List1 ErrorMsg) , HasErr SynthFailed , FileIO @@ -314,6 +317,11 @@ printSynthFailed (UhOh t err) = map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $ prettyNotSynths err +Interpolation (List InkyKind) where + interpolate [] = "end of input" + interpolate [t] = interpolate t + interpolate ts = "one of " ++ joinBy ", " (map interpolate ts) + main : IO () main = run {l = MayThrow} $ @@ -327,6 +335,8 @@ main = (throw . map show . forget) $ handleErr (List1 $ WithBounds String) (throw . map interpolate . forget) $ + handleErr (List1 ParseErr) + (throw . map errToString . forget) $ handleErr (WithBounds String) (throw . (::: [])) $ handleErr IOError @@ -336,7 +346,19 @@ main = printSynthFailed err primIO exitFailure) $ process - --- main = --- run {l = MayThrow} $ --- handle + where + errToString : ParseErr -> String + errToString (BadEOF expected) = "expected \{expected}, got end of input" + errToString (Unexpected expected got) = + interpolate ("expected \{expected}, got \{got.val.kind}" <$ got) + errToString (MapFail e) = + let + msg = + case e.val of + (UnboundTyVar str ctx) => "unbound type variable '\{str}'" + (UnboundTmVar str ctx) => "unbound term variable '\{str}'" + (DuplicateLabel str labels) => "repeated label '\{str}'" + (NeedsSugar mode) => "cannot use syntactic sugar here" + (NeedsQuote mode) => "cannot use splicing here" + NoQuotedTypes => "cannot write types within quotations" + in interpolate (msg <$ e) diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr index 0f05f59..3c13580 100644 --- a/src/Inky/Term.idr +++ b/src/Inky/Term.idr @@ -95,6 +95,10 @@ data Term where Str : (meta : m) -> String -> Term (Sugar qtCtx) m tyCtx tmCtx + FoldCase : + (meta : m) -> Term (Sugar qtCtx) m tyCtx tmCtx -> + Row (x ** Term (Sugar qtCtx) m tyCtx (tmCtx :< x)) -> + Term (Sugar qtCtx) m tyCtx tmCtx %name Term e, f, t, u @@ -122,6 +126,7 @@ export (List meta _).meta = meta (Cons meta _ _).meta = meta (Str meta _).meta = meta +(FoldCase meta _ _).meta = meta -------------------------------------------------------------------------------- -- Well Formed ----------------------------------------------------------------- diff --git a/src/Inky/Term/Desugar.idr b/src/Inky/Term/Desugar.idr index 2ad87c9..53dcec9 100644 --- a/src/Inky/Term/Desugar.idr +++ b/src/Inky/Term/Desugar.idr @@ -1,8 +1,10 @@ module Inky.Term.Desugar import Control.Monad.State +import Data.DPair import Data.SortedMap import Inky.Term +import Inky.Term.Rename -- Other Sugar ----------------------------------------------------------------- @@ -131,6 +133,16 @@ desugar' (Cons meta t u) = let f = cons meta in [| f (desugar' t) (desugar' u) |] desugar' (Str meta str) = string meta str +desugar' (FoldCase meta e (MkRow ts fresh)) = + let + f = \e, ts => + Fold meta e ("__tmp" ** + Case meta (Var meta (toVar Here)) + (fromAll + (mapProperty (map (bimap id (rename Rename.NoSugar (Keep (Drop Thinning.Id))))) ts) + fresh)) + in + [| f (desugar' e) (desugarBranches ts) |] desugarAll [] = pure [] desugarAll (t :: ts) = [| desugar' t :: desugarAll ts |] diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index 5cfd06b..42fd037 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -272,178 +272,109 @@ tokenMap = -- Error Monad ----------------------------------------------------------------- public export -data Result : (a : Type) -> Type where - Ok : a -> Result a - Errs : (msgs : List1 (WithBounds String)) -> Result a +data InkyError : Type where + UnboundTyVar : String -> SnocList String -> InkyError + UnboundTmVar : String -> SnocList String -> InkyError + DuplicateLabel : String -> SnocList String -> InkyError + NeedsSugar : Mode -> InkyError + NeedsQuote : Mode -> InkyError + NoQuotedTypes : InkyError -export -Functor Result where - map f (Ok x) = Ok (f x) - map f (Errs msgs) = Errs msgs - -export -Applicative Result where - pure = Ok - - Ok f <*> Ok x = Ok (f x) - Ok f <*> Errs msgs = Errs msgs - Errs msgs <*> Ok x = Errs msgs - Errs msgs1 <*> Errs msgs2 = Errs (msgs1 ++ msgs2) - -export -Monad Result where - Ok x >>= f = f x - Errs msgs >>= f = Errs msgs - - join (Ok x) = x - join (Errs msgs) = Errs msgs +-- Parser ---------------------------------------------------------------------- -export -extendResult : Row a -> WithBounds (Assoc (Result a)) -> Result (Row a) -extendResult row x = - case (isFresh row.names x.val.name) of - True `Because` prf => Ok ((:<) row (x.val.name :- !x.val.value) @{prf}) - False `Because` _ => - [| const (Errs $ singleton $ "duplicate name \"\{x.val.name}\"" <$ x) x.val.value |] +%inline +public export +TermState : Type +TermState = (Mode, SnocList String, SnocList String) --- Parser ---------------------------------------------------------------------- +%inline +public export +Term' : (Mode, SnocList String, SnocList String) -> Type +Term' state = Term (fst state) Bounds (fst $ snd state) (snd $ snd state) +%inline public export -InkyParser : Bool -> Context Type -> Context Type -> (a : Type) -> Type +InkyParser : + {state : Type} -> (nil : Bool) -> + (locked, free : Context (state -> Type)) -> (a : state -> Type) -> Type InkyParser nil locked free a = - Parser InkyKind nil + Parser state (WithBounds InkyError) InkyKind nil (map (map (False,)) locked) (map (map (False,)) free) a +%inline public export -record ParseFun (as : SnocList Type) (0 p : Fun as Type) where - constructor MkParseFun - try : DFun as (chain (lengthOf as) Parser.Result p) - -mkVar : ({ctx : _} -> Var ctx -> p ctx) -> WithBounds String -> ParseFun [<SnocList String] p -mkVar f x = - MkParseFun - (\ctx => case Var.lookup x.val ctx of - Just i => Ok (f i) - Nothing => Errs (singleton $ "unbound name \"\{x.val}\"" <$ x)) - -mkVar3 : - ({ctx1 : a} -> {ctx2 : b} -> {ctx3 : SnocList String} -> - WithBounds (Var ctx3) -> - p ctx1 ctx2 ctx3) -> - WithBounds String -> ParseFun [<a, b, SnocList String] p -mkVar3 f x = - MkParseFun - (\ctx1, ctx2, ctx3 => case Var.lookup x.val ctx3 of - Just i => Ok (f $ i <$ x) - Nothing => Errs (singleton $ "unbound name \"\{x.val}\"" <$ x)) - -public export -TypeFun : Type -TypeFun = ParseFun [<SnocList String] Ty - -Type'Fun : Type -Type'Fun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Ty' mode Bounds) - -BoundType'Fun : Type -BoundType'Fun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => BoundTy' mode Bounds) - -public export -TermFun : Type -TermFun = ParseFun [<Mode, SnocList String, SnocList String] (\mode => Term mode Bounds) +TypeParser : SnocList String -> SnocList String -> Type +TypeParser locked free = InkyParser False (map (:- Ty) locked) (map (:- Ty) free) Ty +%inline public export -TypeParser : SnocList String -> SnocList String -> Type -TypeParser locked free = - InkyParser False (map (:- TypeFun) locked) (map (:- TypeFun) free) TypeFun +TermParser : SnocList String -> SnocList String -> Type +TermParser locked free = InkyParser False (map (:- Term') locked) (map (:- Term') free) Term' + +mkTyVar : {ctx : _} -> WithBounds String -> Either (WithBounds InkyError) (Ty ctx) +mkTyVar x = + case Var.lookup x.val ctx of + Just i => pure (TVar i) + Nothing => Left (UnboundTyVar x.val ctx <$ x) + +mkTmVar : + {state : _} -> + WithBounds String -> + Either (WithBounds InkyError) (Term' state) +mkTmVar {state = (mode, tyCtx, tmCtx)} x = + case Var.lookup x.val tmCtx of + Just i => pure (Var x.bounds i) + Nothing => Left (UnboundTmVar x.val tmCtx <$ x) RowOf : - (0 free : Context Type) -> + (0 free : Context (state -> Type)) -> InkyParser False [<] free a -> - InkyParser True [<] free (List $ WithBounds $ Assoc a) + InkyParser True [<] free (List . WithBounds . Assoc . a) RowOf free p = - sepBy (match Semicolon) (WithBounds $ mkAssoc <$> Seq [match TypeIdent, match Colon, p]) - where - mkAssoc : HList [String, (), a] -> Assoc a - mkAssoc [x, _, v] = x :- v - -parseRow : - List (WithBounds $ Assoc (ParseFun [<a] p)) -> - ParseFun [<a] (Row . p) -parseRow xs = - MkParseFun (\ctx => - foldlM - (\row => extendResult row . map (\(n :- x) => n :- x.try ctx)) - [<] - xs) - -parseRow3 : - List (WithBounds $ Assoc (ParseFun [<a,b,c] p)) -> - ParseFun [<a, b, c] (\ctx1, ctx2, ctx3 => Row $ p ctx1 ctx2 ctx3) -parseRow3 xs = - MkParseFun (\ctx1, ctx2, ctx3 => - foldlM - (\row => extendResult row . map (\(n :- x) => n :- x.try ctx1 ctx2 ctx3)) - [<] - xs) - -parseList3 : - List (ParseFun [<a,b,c] p) -> - ParseFun [<a, b, c] (\ctx1, ctx2, ctx3 => List $ p ctx1 ctx2 ctx3) -parseList3 [] = MkParseFun (\ctx1, ctx2, ctx3 => Ok []) -parseList3 (x :: xs) = - MkParseFun (\ctx1, ctx2, ctx3 => - [| x.try ctx1 ctx2 ctx3 :: (parseList3 xs).try ctx1 ctx2 ctx3 |]) + sepBy (match Semicolon) + (WithBounds $ (\[x, _, v] => x :- v) <$> Seq [match TypeIdent, match Colon, p]) + +mkRow : + List (WithBounds $ Assoc a) -> + Either (WithBounds InkyError) (Row a) +mkRow = + foldlM + (\row, x => case extend row x.val of + Just row => pure row + Nothing => Left (DuplicateLabel x.val.name row.names <$ x)) + [<] -- Types ----------------------------------------------------------------------- AtomType : TypeParser [<"openType"] [<] AtomType = OneOf - [ mkVar TVar <$> WithBounds (match TypeIdent) - , MkParseFun (\_ => Ok TNat) <$ match Nat - , mkProd <$> enclose (match AngleOpen) (match AngleClose) row - , mkSum <$> enclose (match BracketOpen) (match BracketClose) row + [ Map mkTyVar $ WithBounds (match TypeIdent) + , TNat <$ match Nat + , TProd <$> enclose (match AngleOpen) (match AngleClose) row + , TSum <$> enclose (match BracketOpen) (match BracketClose) row , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openType")) ] where - row : InkyParser True [<] [<"openType" :- TypeFun] (List $ WithBounds $ Assoc TypeFun) - row = RowOf [<"openType" :- TypeFun] $ Var (%%% "openType") - - mkProd : List (WithBounds $ Assoc TypeFun) -> TypeFun - mkProd xs = MkParseFun (\ctx => TProd <$> (parseRow xs).try ctx) - - mkSum : List (WithBounds $ Assoc TypeFun) -> TypeFun - mkSum xs = MkParseFun (\ctx => TSum <$> (parseRow xs).try ctx) + row : InkyParser True [<] [<"openType" :- Ty] (Row . Ty) + row = Map mkRow $ RowOf [<"openType" :- Ty] $ Var (%%% "openType") AppType : TypeParser [<"openType"] [<] AppType = OneOf [ AtomType - , match List **> mkList <$> weaken (S Z) AtomType - , mkFix <$> Seq - [ match Data - , match TypeIdent - , weaken (S Z) AtomType - ] + , match List *> TList <$> weaken (S Z) AtomType + , match Data *> (\[x, t] => TFix x t) <$> + Seq (Update (match TypeIdent) (Just (:<)) [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 = - Fix "openType" $ mkArrow <$> sepBy1 (match Arrow) AppType - where - mkArrow : List1 TypeFun -> TypeFun - mkArrow = - foldr1 {a = TypeFun} - (\x, y => MkParseFun (\ctx => [| TArrow (x.try ctx) (y.try ctx) |])) + Fix "openType" $ foldr1 TArrow <$> sepBy1 (match Arrow) AppType export [ListSet] Eq a => Set a (List a) where @@ -462,483 +393,329 @@ OpenTypeWf = Refl -- Terms ----------------------------------------------------------------------- -NoSugarMsg : String -NoSugarMsg = "sugar is not allowed here" - -NoUnquoteMsg : String -NoUnquoteMsg = "cannot unquote outside of quote" - -NoQuoteMsg : String -NoQuoteMsg = "cannot quote inside of quote" - -NoQuoteTypesMsg : String -NoQuoteTypesMsg = "cannot quote types" - -NoLetTyMsg : String -NoLetTyMsg = "cannot bind type inside of quote" - -NoQAbsMsg : String -NoQAbsMsg = "cannot bind term name inside of quote" - -AtomTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +Type' : (Mode, SnocList String, SnocList String) -> Type +Type' state = Ty' (fst state) Bounds (fst $ snd state) (snd $ snd state) + +BoundType' : (Mode, SnocList String, SnocList String) -> Type +BoundType' state = BoundTy' (fst state) Bounds (fst $ snd state) (snd $ snd state) + +sugarOnly : + (0 a, b : (Mode, SnocList String, SnocList String) -> Type) -> + ({qtCtx, tyCtx, tmCtx : _} -> + WithBounds (a (Sugar qtCtx, tyCtx, tmCtx)) -> + b (Sugar qtCtx, tyCtx, tmCtx)) -> + {state : _} -> WithBounds (a state) -> Either (WithBounds InkyError) (b state) +sugarOnly a b f {state = (Sugar qtCtx, tyCtx, tmCtx)} x = pure (f x) +sugarOnly a b f {state = (mode, tyCtx, tmCtx)} x = Left (NeedsSugar mode <$ x) + +quoteOnly : + (0 a, b : (Mode, SnocList String, SnocList String) -> Type) -> + ({ctx1, ctx2, tmCtx : _} -> + WithBounds (a (Quote ctx1 ctx2, [<], tmCtx)) -> + b (Quote ctx1 ctx2, [<], tmCtx)) -> + {state : _} -> WithBounds (a state) -> Either (WithBounds InkyError) (b state) +-- HACK: should special case for tyCtx /= [<]. But this case is "impossible", so it doesn't matter +quoteOnly a b f {state = (Quote ctx1 ctx2, [<], tmCtx)} x = pure (f x) +quoteOnly a b f {state = (mode, tyCtx, tmCtx)} x = Left (NeedsQuote mode <$ x) + +forceQuote : + (Mode, SnocList String, SnocList String) -> (Mode, SnocList String, SnocList String) +forceQuote (Sugar qtCtx, tyCtx, tmCtx) = (Quote tyCtx tmCtx, [<], qtCtx) +forceQuote state = state + +forceSugar : + (Mode, SnocList String, SnocList String) -> (Mode, SnocList String, SnocList String) +forceSugar (Quote ctx1 ctx2, tyCtx, tmCtx) = (Sugar tmCtx, ctx1, ctx2) +forceSugar state = state + +embedType : + {state : _} -> + WithBounds (Ty (fst $ snd state)) -> + Either (WithBounds InkyError) (Type' state) +embedType {state = (Quote ctx1 ctx2, tyCtx, tmCtx)} t = Left (NoQuotedTypes <$ t) +embedType {state = (Sugar qtCtx, tyCtx, tmCtx)} t = Right t.val +embedType {state = (NoSugar, tyCtx, tmCtx)} t = Right t.val + +AtomTerm : TermParser [<"openTerm"] [<] AtomTerm = OneOf - [ mkVar3 (\x => Var x.bounds x.val) <$> WithBounds (match TermIdent) - , mkStrLit <$> WithBounds (match StringLit) - , mkLit <$> WithBounds (match Lit) - , mkList <$> WithBounds ( + [ Map mkTmVar $ WithBounds (match TermIdent) + , Map (sugarOnly (const String) Term' (\k => Str k.bounds k.val)) $ + WithBounds (match StringLit) + , Map (sugarOnly (const Nat) Term' (\k => Lit k.bounds k.val)) $ + WithBounds (match Lit) + , Map (sugarOnly (List . Term') Term' (\ts => List ts.bounds ts.val)) $ WithBounds ( enclose (match BracketOpen) (match BracketClose) $ - sepBy (match Semicolon) $ - Var (%%% "openTerm")) - , mkTup <$> WithBounds (enclose (match AngleOpen) (match AngleClose) $ - RowOf [<"openTerm" :- TermFun] (Var (%%% "openTerm"))) + sepBy (match Semicolon) $ Var (%%% "openTerm")) + , (\row => Tup row.bounds row.val) <$> WithBounds ( + enclose (match AngleOpen) (match AngleClose) $ + Map mkRow $ RowOf [<"openTerm" :- Term'] (Var (%%% "openTerm"))) , enclose (match ParenOpen) (match ParenClose) (Var (%%% "openTerm")) ] - where - mkStrLit : WithBounds String -> TermFun - mkStrLit k = MkParseFun (\mode, tyCtx, tmCtx => - case mode of - NoSugar => Errs (singleton $ NoSugarMsg <$ k) - Sugar qtCtx => Ok (Str k.bounds k.val) - Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ k)) - - mkLit : WithBounds Nat -> TermFun - mkLit k = MkParseFun (\mode, tyCtx, tmCtx => - case mode of - NoSugar => Errs (singleton $ NoSugarMsg <$ k) - Sugar qtCtx => Ok (Lit k.bounds k.val) - Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ k)) - mkList : WithBounds (List TermFun) -> TermFun - mkList xs = MkParseFun (\mode, tyCtx, tmCtx => - case mode of - NoSugar => Errs (singleton $ NoSugarMsg <$ xs) - Sugar ctx => List xs.bounds <$> (parseList3 xs.val).try (Sugar ctx) tyCtx tmCtx - Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ xs)) - - mkTup : WithBounds (List (WithBounds $ Assoc TermFun)) -> TermFun - mkTup xs = - MkParseFun (\mode, tyCtx, tmCtx => - Tup xs.bounds <$> (parseRow3 xs.val).try mode tyCtx tmCtx) - -PrefixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +PrefixTerm : TermParser [<"openTerm"] [<] PrefixTerm = Fix "prefixTerm" $ OneOf - [ mkRoll <$> WithBounds (match Tilde **> Var (%%% "prefixTerm")) - , mkUnroll <$> WithBounds (match Bang **> Var (%%% "prefixTerm")) - , mkQuote <$> WithBounds (match Backtick **> Var (%%% "prefixTerm")) - , mkUnquote <$> WithBounds (match Comma **> Var (%%% "prefixTerm")) + [ (\t => Roll t.bounds t.val) <$> WithBounds (match Tilde *> Var (%%% "prefixTerm")) + , (\t => Unroll t.bounds t.val) <$> WithBounds (match Bang *> Var (%%% "prefixTerm")) + , Map (sugarOnly (Term' . forceQuote) Term' (\t => QuasiQuote t.bounds t.val)) $ + WithBounds $ (\[_, t] => t) <$> + Seq (Update (match Backtick) (Just $ const . forceQuote) [Var (%%% "prefixTerm")]) + , Map (quoteOnly (Term' . forceSugar) Term' (\t => Unquote t.bounds t.val)) $ + WithBounds $ (\[_, t] => t) <$> + Seq (Update (match Comma) (Just $ const . forceSugar) [Var (%%% "prefixTerm")]) , rename (Drop Id) Id AtomTerm ] - where - mkRoll : WithBounds TermFun -> TermFun - mkRoll x = MkParseFun (\mode, tyCtx, tmCtx => Roll x.bounds <$> x.val.try mode tyCtx tmCtx) - - mkUnroll : WithBounds TermFun -> TermFun - mkUnroll x = MkParseFun (\mode, tyCtx, tmCtx => Unroll x.bounds <$> x.val.try mode tyCtx tmCtx) - - mkQuote : WithBounds TermFun -> TermFun - mkQuote x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoQuoteMsg <$ x) - Sugar ctx => QuasiQuote x.bounds <$> x.val.try (Quote tyCtx tmCtx) [<] ctx - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - - mkUnquote : WithBounds TermFun -> TermFun - mkUnquote x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => - case tyCtx of - [<] => Unquote x.bounds <$> x.val.try (Sugar tmCtx) ctx1 ctx2 - _ => Errs (singleton $ "internal error 0001" <$ x) - Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x) - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - -SuffixTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun -SuffixTerm = mkSuffix <$> Seq [ PrefixTerm , star (match Dot **> WithBounds (match TypeIdent)) ] - where - mkSuffix : HList [TermFun, List (WithBounds String)] -> TermFun - mkSuffix [t, []] = t - mkSuffix [t, prjs] = - MkParseFun (\mode, tyCtx, tmCtx => - Ok $ foldl (\acc, l => Prj l.bounds acc l.val) !(t.try mode tyCtx tmCtx) prjs) -SuffixTy' : InkyParser False [<"openTerm" :- TermFun] [<] Type'Fun +SuffixTerm : TermParser [<"openTerm"] [<] +SuffixTerm = + (\[t, prjs] => foldl (\t, l => Prj l.bounds t l.val) t prjs) <$> + Seq [PrefixTerm , star (match Dot *> WithBounds (match TypeIdent)) ] + +SuffixTy' : InkyParser False [<"openTerm" :- Term'] [<] Type' SuffixTy' = OneOf - [ mkTy <$> WithBounds (sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType) - , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm) + [ Map embedType $ Forget (fst . snd) $ WithBounds $ sub [<"openType" :- OpenType] [<] AtomType + , Map (quoteOnly (Term' . forceSugar) Type' val) $ + WithBounds $ (\[_, t] => t) <$> + Seq (Update (match Comma) (Just $ const . forceSugar) [weaken (S Z) PrefixTerm]) ] - where - mkTy : WithBounds TypeFun -> Type'Fun - mkTy x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x) - Sugar ctx => x.val.try tyCtx - NoSugar => x.val.try tyCtx) - - mkTm : WithBounds TermFun -> Type'Fun - mkTm x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2 - Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x) - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - -SuffixBoundTy' : InkyParser False [<"openTerm" :- TermFun] [<] BoundType'Fun + +SuffixBoundTy' : InkyParser False [<"openTerm" :- Term'] [<] BoundType' SuffixBoundTy' = - OneOf - [ mkTy <$> enclose (match ParenOpen) (match ParenClose) (Seq - [ WithBounds (match Backslash) - , match TypeIdent - , match DoubleArrow - , rename Id (Drop Id) OpenType - ]) - , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm) + OneOf {nils = [False, False]} + [ enclose (match ParenOpen) (match ParenClose) $ + Map embedBoundType $ + Forget (fst . snd) $ + WithBounds {a = \ctx => (x ** Ty (ctx :< x))} $ + (\[n, t] => (n ** t)) <$> + Seq (Update (match Backslash *> match TypeIdent <* match DoubleArrow) (Just (:<)) [OpenType]) + , Map (quoteOnly (Term' . forceSugar) BoundType' val) $ + WithBounds $ (\[_, t] => t) <$> + Seq (Update (match Comma) (Just $ const . forceSugar) [weaken (S Z) PrefixTerm]) ] where - mkTy : HList [WithBounds _, String, _, TypeFun] -> BoundType'Fun - mkTy [x, n, _, a] = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x) - Sugar ctx => MkDPair n <$> a.try (tyCtx :< n) - NoSugar => MkDPair n <$> a.try (tyCtx :< n)) - - mkTm : WithBounds TermFun -> BoundType'Fun - mkTm x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2 - Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x) - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - -AppTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun + embedBoundType : + {state : _} -> + WithBounds (x ** Ty (fst (snd state) :< x)) -> + Either (WithBounds InkyError) (BoundType' state) + embedBoundType {state = (Quote ctx1 ctx2, tyCtx, tmCtx)} t = Left (NoQuotedTypes <$ t) + embedBoundType {state = (Sugar qtCtx, tyCtx, tmCtx)} t = Right t.val + embedBoundType {state = (NoSugar, tyCtx, tmCtx)} t = Right t.val + +AppTerm : TermParser [<"openTerm"] [<] AppTerm = OneOf - [ mkInj <$> Seq - [ 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 - , mkMap <$> Seq - [ WithBounds (match Map) - , weaken (S Z) SuffixBoundTy' - , weaken (S Z) SuffixTy' - , weaken (S Z) SuffixTy' + [ (\lt => Inj lt.bounds (fst lt.val) (snd lt.val)) <$> + WithBounds (match TypeIdent <**> weaken (S Z) SuffixTerm) + , Map (sugarOnly Term' Term' (\t => Suc t.bounds t.val)) $ + WithBounds $ match Suc *> weaken (S Z) SuffixTerm + , Map (sugarOnly (\s => (Term' s, Term' s)) Term' + (\tu => Cons tu.bounds (fst tu.val) (snd tu.val))) $ + WithBounds $ match Cons *> weaken (S Z) SuffixTerm <**> weaken (S Z) SuffixTerm + , (\case + [f, []] => f.val + [f, args] => App f.bounds f.val args) <$> + Seq + [ OneOf + [ WithBounds SuffixTerm + , (\[x, f, a, b] => Map x.bounds f a b <$ x) <$> Seq + [ WithBounds (match Map) + , weaken (S Z) SuffixBoundTy' + , weaken (S Z) SuffixTy' + , weaken (S Z) SuffixTy' + ] ] + , star (weaken (S Z) SuffixTerm) ] - , star (weaken (S Z) SuffixTerm) - ] ] - where - mkInj : HList [WithBounds String, TermFun] -> TermFun - mkInj [tag, t] = - MkParseFun (\mode, tyCtx, tmCtx => - Inj tag.bounds tag.val <$> t.try mode tyCtx tmCtx) - - mkSuc : HList [WithBounds _, TermFun] -> TermFun - mkSuc [x, t] = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ x) - Sugar ctx => Suc x.bounds <$> t.try (Sugar ctx) tyCtx tmCtx - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - - mkCons : HList [WithBounds _, TermFun, TermFun] -> TermFun - mkCons [x, t, u] = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoSugarMsg <$ x) - Sugar ctx => - [| Cons (pure x.bounds) - (t.try (Sugar ctx) tyCtx tmCtx) - (u.try (Sugar ctx) tyCtx tmCtx) - |] - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - - mkMap : - HList [WithBounds (), BoundType'Fun, Type'Fun, Type'Fun] -> - WithBounds TermFun - mkMap [m, a, b, c] = - MkParseFun (\mode, tyCtx, tmCtx => do - (a, b, c) <- - [| (a.try mode tyCtx tmCtx, [|(b.try mode tyCtx tmCtx, c.try mode tyCtx tmCtx)|]) |] - Ok $ Map m.bounds a b c) - <$ m - - mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun - mkApp [t, []] = t.val - mkApp [fun, args] = - MkParseFun (\mode, tyCtx, tmCtx => do - (funVal, args) <- - [| (fun.val.try mode tyCtx tmCtx, (parseList3 args).try mode tyCtx tmCtx) |] - Ok $ App fun.bounds funVal args) - -OpenTy' : InkyParser False [<"openTerm" :- TermFun] [<] Type'Fun + +OpenTy' : InkyParser False [<"openTerm" :- Term'] [<] Type' OpenTy' = OneOf - [ mkTy <$> WithBounds (rename (Drop Id) Id OpenType) - , mkTm <$> WithBounds (match Comma **> weaken (S Z) PrefixTerm) - ] - where - mkTy : WithBounds TypeFun -> Type'Fun - mkTy x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoQuoteTypesMsg <$ x) - Sugar ctx => x.val.try tyCtx - NoSugar => x.val.try tyCtx) - - mkTm : WithBounds TermFun -> Type'Fun - mkTm x = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => x.val.try (Sugar tmCtx) ctx1 ctx2 - Sugar ctx => Errs (singleton $ NoUnquoteMsg <$ x) - NoSugar => Errs (singleton $ NoSugarMsg <$ x)) - -AnnotTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun -AnnotTerm = - mkAnnot <$> Seq - [ AppTerm - , option (match Colon **> WithBounds (weaken (S Z) OpenTy')) + [ Map embedType $ Forget (fst . snd) $ WithBounds OpenType + , Map (quoteOnly (Term' . forceSugar) Type' val) $ + WithBounds $ (\[_, t] => t) <$> + Seq (Update (match Comma) (Just $ const . forceSugar) [weaken (S Z) PrefixTerm]) ] - where - mkAnnot : HList [TermFun, Maybe (WithBounds Type'Fun)] -> TermFun - mkAnnot [t, Nothing] = t - mkAnnot [t, Just a] = MkParseFun (\mode, tyCtx, tmCtx => - [| Annot (pure a.bounds) (t.try mode tyCtx tmCtx) (a.val.try mode tyCtx tmCtx) |]) -- Open Terms -LetTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun +AnnotTerm : TermParser [<"openTerm"] [<] +AnnotTerm = + (\case + (t, Nothing) => t + (t, Just a) => Annot a.bounds t a.val) <$> + (AppTerm <**> option (WithBounds $ match Colon *> weaken (S Z) OpenTy')) + +LetTerm : TermParser [<"openTerm"] [<] LetTerm = - match Let **> + match Let *> OneOf - [ mkLet <$> Seq - [ WithBounds (match TermIdent) - , OneOf - [ mkAnnot <$> Seq - [ star (enclose (match ParenOpen) (match ParenClose) $ - Seq [ match TermIdent, match Colon, weaken (S Z) OpenTy' ]) - , WithBounds (match Colon) - , weaken (S Z) OpenTy' - , match Equal - , star (match Comment) - , Var (%%% "openTerm")] - , mkUnannot <$> Seq [match Equal, star (match Comment) , Var (%%% "openTerm")] - ] - , match In - , Var (%%% "openTerm") - ] - , mkLetType <$> Seq - [ WithBounds (match TypeIdent) - , match Equal - , star (match Comment) - , rename Id (Drop Id) OpenType - , match In - , Var (%%% "openTerm") - ] + [ mkLet _ <$> Seq + (Update + (WithBounds (match TermIdent) <**> OneOf + [ mkAnnot _ <$> + Seq (Update + (Seq + [ star (enclose (match ParenOpen) (match ParenClose) + (match TermIdent <* match Colon <**> weaken (S Z) OpenTy')) + , WithBounds (match Colon) + , weaken (S Z) OpenTy' + , match Equal + , star (match Comment) + ]) + (Just GetArgs) + [Var (%%% "openTerm")]) + , (\[_, doc, body] => AddDoc body doc) <$> + Seq [match Equal, star (match Comment), Var (%%% "openTerm")] + ]) + (Just $ \state, v => mapSnd (mapSnd (:< (fst v).val)) state) + [match In *> Var (%%% "openTerm")]) + , Map (mkLetTy _) $ Seq + (Update + (WithBounds (match TypeIdent) <**> + uncurry (flip AddDoc) <$> + (match Equal *> (star (match Comment) <**> Forget (fst . snd) OpenType))) + (Just $ \state, v => mapSnd (mapFst (:< (fst v).val)) state) + [match In *> Var (%%% "openTerm")]) + ] where - mkLet : HList [WithBounds String, WithDoc TermFun, (), TermFun] -> TermFun - mkLet [x, AddDoc e doc, _, t] = - MkParseFun (\mode, tyCtx, tmCtx => - [| (\e, t => Let (AddDoc x.bounds doc) e (x.val ** t)) - (e.try mode tyCtx tmCtx) - (t.try mode tyCtx (tmCtx :< x.val)) - |]) - - mkLetType : HList [WithBounds String, (), List String, TypeFun, (), TermFun] -> TermFun - mkLetType [x, _, doc, a, _, t] = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoLetTyMsg <$ x) - Sugar ctx => - [| (\a, t => LetTy (AddDoc x.bounds doc) a (x.val ** t)) - (a.try tyCtx) - (t.try (Sugar ctx) (tyCtx :< x.val) tmCtx) - |] - NoSugar => - [| (\a, t => LetTy (AddDoc x.bounds doc) a (x.val ** t)) - (a.try tyCtx) - (t.try NoSugar (tyCtx :< x.val) tmCtx) - |]) - - mkArrow : (meta : Bounds) -> List Type'Fun -> Type'Fun -> Type'Fun - mkArrow meta [] cod = cod - mkArrow meta (arg :: args) cod = - let - arrowTm : - Term mode Bounds tyCtx tmCtx -> - Term mode Bounds tyCtx tmCtx -> - Term mode Bounds tyCtx tmCtx - arrowTm = - \t, u => Roll meta $ Inj meta "TArrow" $ Tup meta [<"Dom" :- t, "Cod" :- u] - in - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => - [| arrowTm - (arg.try (Quote ctx1 ctx2) tyCtx tmCtx) - ((mkArrow meta args cod).try (Quote ctx1 ctx2) tyCtx tmCtx) - |] - Sugar ctx => - [| TArrow - (arg.try (Sugar ctx) tyCtx tmCtx) - ((mkArrow meta args cod).try (Sugar ctx) tyCtx tmCtx) - |] - NoSugar => - [| TArrow - (arg.try NoSugar tyCtx tmCtx) - ((mkArrow meta args cod).try NoSugar tyCtx tmCtx) - |]) + AnnotSeq : List (Stage TermState) + AnnotSeq = map (\a => MkStage a Nothing) + [ (\s => List (String, Type' s)) + , const (WithBounds ()) + , Type' + , const () + , const (List String) + ] - mkAnnot : - HList [List (HList [String, (), Type'Fun]), WithBounds (), Type'Fun, (), List String, TermFun] -> - WithDoc TermFun - mkAnnot [[], m, cod, _, doc, t] = - AddDoc - (MkParseFun (\mode, tyCtx, tmCtx => - [| Annot (pure m.bounds) (t.try mode tyCtx tmCtx) (cod.try mode tyCtx tmCtx) |])) - doc - mkAnnot [args, m, cod, _, doc, t] = - let bound = map (\[x, _, a] => x) args in - let tys = map (\[x, _, a] => a) args in - AddDoc - (MkParseFun (\mode, tyCtx, tmCtx => - [| (\t, a => Annot m.bounds (Abs m.bounds (bound ** t)) a) - (t.try mode tyCtx (tmCtx <>< bound)) - ((mkArrow m.bounds tys cod).try mode tyCtx tmCtx) - |])) - doc + LetSeq : List (Stage TermState) + LetSeq = + [ MkStage (\s => (WithBounds String, WithDoc (Term' s))) + (Just $ \s, v => mapSnd (mapSnd (:< (fst v).val)) s) + , MkStage Term' Nothing + ] + + LetTySeq : List (Stage TermState) + LetTySeq = + [ MkStage (\s => (WithBounds String, WithDoc (Ty $ fst $ snd s))) + (Just $ \s, v => mapSnd (mapFst (:< (fst v).val)) s) + , MkStage Term' Nothing + ] + + GetArgs : (state : TermState) -> Sequence state AnnotSeq -> TermState + GetArgs state [args, _, _, _, _] = mapSnd (mapSnd (<>< map fst args)) state - mkUnannot : HList [(), List String, TermFun] -> WithDoc TermFun - mkUnannot [_, doc, e] = AddDoc e doc + MkArrow : (meta : Bounds) -> (state : TermState) -> Type' state -> Type' state -> Type' state + MkArrow meta (Quote ctx1 ctx2, _, _) = \dom, cod => + Roll meta $ Inj meta "TArrow" $ Tup meta [<"Dom" :- dom, "Cod" :- cod] + MkArrow meta (Sugar qtCtx, _, _) = TArrow + MkArrow meta (NoSugar, _, _) = TArrow -AbsTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun + mkAnnot : + (state : TermState) -> + Sequence state [MkStage (flip Sequence AnnotSeq) (Just GetArgs), MkStage Term' Nothing] -> + WithDoc (Term' state) + mkAnnot (_, _, _) [[[], colon, ret, _, docs], body] = + AddDoc (Annot colon.bounds body ret) docs + mkAnnot (mode, tyCtx, tmCtx) [[(arg :: args), colon, ret, _, docs], body] = + AddDoc + (Annot colon.bounds + (Abs colon.bounds (fst arg :: map fst args ** body)) + (foldr (MkArrow colon.bounds (mode, tyCtx, tmCtx)) ret (snd arg ::: map snd args))) + docs + + mkLet : (state : TermState) -> Sequence state LetSeq -> Term' state + mkLet (_, _, _) [(x, body), rest] = Let (AddDoc x.bounds body.doc) body.value (x.val ** rest) + + mkLetTy : + (state : TermState) -> + Sequence state LetTySeq -> + Either (WithBounds InkyError) (Term' state) + mkLetTy (Quote ctx1 ctx2, _, _) [(x, ty), rest] = Left (NoQuotedTypes <$ x) + mkLetTy (Sugar qtCtx, _, _) [(x, ty), rest] = + pure $ LetTy (AddDoc x.bounds ty.doc) ty.value (x.val ** rest) + mkLetTy (NoSugar, _, _) [(x, ty), rest] = + pure $ LetTy (AddDoc x.bounds ty.doc) ty.value (x.val ** rest) + +AbsTerm : TermParser [<"openTerm"] [<] AbsTerm = - mkAbs <$> Seq - [ WithBounds (match Backslash) - , sepBy1 (match Comma) (match TermIdent) - , (match DoubleArrow <||> match WaveArrow) - , Var (%%% "openTerm") - ] + Map (mkAbs _) $ + Seq + (Update + (WithBounds (match Backslash *> sepBy1 (match Comma) (match TermIdent)) <**> + (match DoubleArrow <||> match WaveArrow)) + (Just UpdateCtx) + [Var (%%% "openTerm")]) where - mkAbs : HList [WithBounds (), List1 String, Either () (), TermFun] -> TermFun - mkAbs [m, args, Left _, body] = - MkParseFun (\mode, tyCtx, tmCtx => - [| (\t => Abs m.bounds (forget args ** t)) - (body.try mode tyCtx (tmCtx <>< forget args)) - |]) - mkAbs [m, args, Right _, body] = - MkParseFun (\mode, tyCtx, tmCtx => - case mode of - Quote ctx1 ctx2 => Errs (singleton $ NoQAbsMsg <$ m) - Sugar ctx => - [| (\t => QAbs m.bounds (forget args ** t)) - (body.try (Sugar (ctx <>< forget args)) tyCtx tmCtx) - |] - NoSugar => Errs (singleton $ NoSugarMsg <$ m)) - -CaseTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun + UpdateCtx : (state : TermState) -> (WithBounds (List1 String), Either () ()) -> TermState + UpdateCtx state (args, Left abs) = mapSnd (mapSnd (<>< forget args.val)) state + UpdateCtx state (args, Right quot) = case fst state of + Sugar qtCtx => (Sugar (qtCtx <>< forget args.val), snd state) + _ => state + + mkAbs : + (state : TermState) -> + Sequence state + [ MkStage (const $ (WithBounds (List1 String), Either () ())) (Just UpdateCtx) + , MkStage Term' Nothing + ] -> + Either (WithBounds InkyError) (Term' state) + mkAbs (mode, tyCtx, tmCtx) [(args, Left abs), body] = pure (Abs args.bounds (forget args.val ** body)) + mkAbs (mode, tyCtx, tmCtx) [(args, Right quot), body] = + case mode of + Sugar qtCtx => pure (QAbs args.bounds (forget args.val ** body)) + _ => Left (NeedsSugar mode <$ args) + +CaseTerm : TermParser [<"openTerm"] [<] CaseTerm = - (\[f, x] => f x) <$> - Seq - [ OneOf - [ mkCase <$> Seq - [ WithBounds (match Case) - , Var (%%% "openTerm") - , match Of - ] - , mkFoldCase <$> Seq - [ WithBounds (match FoldCase) - , Var (%%% "openTerm") - , match By - ] - ] - , enclose (match BraceOpen) (match BraceClose) ( - sepBy (match Semicolon) $ + Map (uncurry $ mkCase _) $ + WithBounds ( + (match Case *> Var (%%% "openTerm") <* match Of) <||> + (match FoldCase *> Var (%%% "openTerm") <* match By)) + <**> Map mkRow + (enclose (match BraceOpen) (match BraceClose) + (sepBy (match Semicolon) $ WithBounds $ - Seq - [ match TypeIdent - , match TermIdent - , match DoubleArrow - , Var (%%% "openTerm") - ]) - ] + (\[(label, x), body] => label :- (x ** body)) <$> + Seq (Update + (match TypeIdent <**> match TermIdent <* match DoubleArrow) + (Just $ \state, x => mapSnd (mapSnd (:< snd x)) state) + [Var (%%% "openTerm")]))) where - Cases : Type - Cases = List (WithBounds $ HList [String, String, (), TermFun]) - - mkBranch : - HList [String, String, (), TermFun] -> - Assoc - (ParseFun [<Mode, SnocList String, SnocList String] $ - \mode, tyCtx, tmCtx => (x ** Term mode Bounds tyCtx (tmCtx :< x))) - mkBranch [tag, bound, _, branch] = - tag :- - MkParseFun (\mode, tyCtx, tmCtx => - [| (\t => MkDPair bound t) (branch.try mode tyCtx (tmCtx :< bound)) |]) - - mkCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun - mkCase [m, target, _] branches = - let branches = map (map mkBranch) branches in - MkParseFun (\mode, tyCtx, tmCtx => - [| Case (pure m.bounds) - (target.try mode tyCtx tmCtx) - ((parseRow3 branches).try mode tyCtx tmCtx) - |]) - - mkFoldCase : HList [WithBounds (), TermFun, _] -> Cases -> TermFun - mkFoldCase [m, target, _] branches = - let branches = map (map mkBranch) branches in - MkParseFun (\mode, tyCtx, tmCtx => - [| (\t, ts => Fold m.bounds t ("__tmp" ** Case m.bounds (Var m.bounds $ %% "__tmp") ts)) - (target.try mode tyCtx tmCtx) - ((parseRow3 branches).try mode tyCtx (tmCtx :< "__tmp")) - |]) - -FoldTerm : InkyParser False [<"openTerm" :- TermFun] [<] TermFun + mkCase : + (state : TermState) -> + WithBounds (Either (Term' state) (Term' state)) -> + Row (x ** Term' (mapSnd (mapSnd (:< x)) state)) -> + Either (WithBounds InkyError) (Term' state) + mkCase (mode, _, _) x branches = case x.val of + Left target => pure $ Case x.bounds target branches + Right target => case mode of + Sugar _ => pure $ FoldCase x.bounds target branches + _ => Left (NeedsSugar mode <$ x) + +FoldTerm : TermParser [<"openTerm"] [<] FoldTerm = - mkFold <$> Seq - [ WithBounds (match Fold) - , Var (%%% "openTerm") - , match By - , enclose (match ParenOpen) (match ParenClose) $ - Seq - [ match Backslash - , match TermIdent - , match DoubleArrow - , Var (%%% "openTerm") - ] - ] + mkFold _ <$> + ( WithBounds (match Fold *> Var (%%% "openTerm") <* match By) + <**> + (\[x, u] => (x ** u)) <$> + enclose (match ParenOpen) (match ParenClose) + (Seq $ Update + (match Backslash *> match TermIdent <* match DoubleArrow) + (Just $ \state, x => mapSnd (mapSnd (:< x)) state) + [Var (%%% "openTerm")])) where - mkFold : HList [WithBounds (), TermFun, (), HList [(), String, (), TermFun]] -> TermFun - mkFold [m, target, _, [_, arg, _, body]] = - MkParseFun (\mode, tyCtx, tmCtx => - [| (\e, t => Fold m.bounds e (arg ** t)) - (target.try mode tyCtx tmCtx) - (body.try mode tyCtx (tmCtx :< arg)) - |]) + mkFold : + (state : TermState) -> + (WithBounds (Term' state), (x ** Term' (mapSnd (mapSnd (:< x)) state))) -> + Term' state + mkFold (_, _, _) (t, rest) = Fold t.bounds t.val rest export -OpenTerm : InkyParser False [<] [<] TermFun +OpenTerm : TermParser [<] [<] OpenTerm = Fix "openTerm" $ OneOf [ LetTerm diff --git a/src/Inky/Term/Pretty.idr b/src/Inky/Term/Pretty.idr index fbedab3..041eb42 100644 --- a/src/Inky/Term/Pretty.idr +++ b/src/Inky/Term/Pretty.idr @@ -188,14 +188,6 @@ prettyTerm (Roll _ t) d = parenthesise (d < Prefix) $ align $ pretty "~" <+> prettyTerm t Prefix prettyTerm (Unroll _ e) d = parenthesise (d < Prefix) $ align $ pretty "!" <+> prettyTerm e Prefix -prettyTerm (Fold _ e ("__tmp" ** Case _ (Var _ ((%%) "__tmp" {pos = Here})) (MkRow ts _))) d = - let parts = prettyCases ts <>> [] in - -- XXX: should check for usage of "__tmp" in ts - group $ align $ hang 2 $ parenthesise (d < Open) $ - (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+> - (braces $ flatAlt - (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line) - (concatWith (surround $ ";" <++> neutral) parts)) prettyTerm (Fold _ e (x ** t)) d = group $ align $ hang 2 $ parenthesise (d < Open) $ (group $ hang (-2) $ "fold" <++> prettyTerm e Open <++> "by") <+> line <+> @@ -231,3 +223,10 @@ prettyTerm (Cons _ t u) d = group $ align $ hang 2 $ parenthesise (d < App) $ concatWith (surround line) [pretty "cons", prettyTerm t Suffix, prettyTerm u Suffix] prettyTerm (Str _ str) d = enclose "\"" "\"" $ pretty str +prettyTerm (FoldCase _ e (MkRow ts _)) d = + let parts = prettyCases ts <>> [] in + group $ align $ hang 2 $ parenthesise (d < Open) $ + (group $ "foldcase" <++> prettyTerm e Open <++> "by") <+> line <+> + (braces $ flatAlt + (neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line) + (concatWith (surround $ ";" <++> neutral) parts)) diff --git a/src/Inky/Term/Rename.idr b/src/Inky/Term/Rename.idr new file mode 100644 index 0000000..7bbd524 --- /dev/null +++ b/src/Inky/Term/Rename.idr @@ -0,0 +1,85 @@ +module Inky.Term.Rename + +import Inky.Term +import Flap.Data.List +import Flap.Data.SnocList.Thinning + +public export +data Thins : Mode -> Mode -> Type where + NoSugar : NoSugar `Thins` NoSugar + Sugar : qtCtx1 `Thins` qtCtx2 -> Sugar qtCtx1 `Thins` Sugar qtCtx2 + Quote : ctx2 `Thins` ctx3 -> Quote ctx1 ctx2 `Thins` Quote ctx1 ctx3 + +export +rename : + mode `Thins` mode' -> tmCtx `Thins` tmCtx' -> + Term mode meta tyCtx tmCtx -> + Term mode' meta tyCtx tmCtx' +renameList : + mode `Thins` mode' -> tmCtx `Thins` tmCtx' -> + List (Term mode meta tyCtx tmCtx) -> + List (Term mode' meta tyCtx tmCtx') +renameAll : + mode `Thins` mode' -> tmCtx `Thins` tmCtx' -> + (ts : Context (Term mode meta tyCtx tmCtx)) -> + All (Assoc0 $ Term mode' meta tyCtx tmCtx') ts.names +renameBranches : + mode `Thins` mode' -> tmCtx `Thins` tmCtx' -> + (ts : Context (x ** Term mode meta tyCtx (tmCtx :< x))) -> + All (Assoc0 (x ** Term mode' meta tyCtx (tmCtx' :< x))) ts.names +renameTy' : + mode `Thins` mode' -> tmCtx `Thins` tmCtx' -> + Ty' mode meta tyCtx tmCtx -> + Ty' mode' meta tyCtx tmCtx' +renameBoundTy' : + mode `Thins` mode' -> tmCtx `Thins` tmCtx' -> + BoundTy' mode meta tyCtx tmCtx -> + BoundTy' mode' meta tyCtx tmCtx' + +rename f g (Annot m e a) = Annot m (rename f g e) (renameTy' f g a) +rename f g (Var m i) = Var m (index g i) +rename f g (Let m e (x ** t)) = Let m (rename f g e) (x ** rename f (Keep g) t) +rename f g (LetTy m a (x ** t)) = + case f of + NoSugar => LetTy m a (x ** rename f g t) + Sugar _ => LetTy m a (x ** rename f g t) +rename f g (Abs m (bound ** t)) = Abs m (bound ** rename f (g <>< lengthOf bound) t) +rename f g (App m e ts) = App m (rename f g e) (renameList f g ts) +rename f g (Tup m (MkRow ts fresh)) = Tup m (fromAll (renameAll f g ts) fresh) +rename f g (Prj m e l) = Prj m (rename f g e) l +rename f g (Inj m l t) = Inj m l (rename f g t) +rename f g (Case m e (MkRow ts fresh)) = + Case m (rename f g e) (fromAll (renameBranches f g ts) fresh) +rename f g (Roll m t) = Roll m (rename f g t) +rename f g (Unroll m e) = Unroll m (rename f g e) +rename f g (Fold m e (x ** t)) = Fold m (rename f g e) (x ** rename f (Keep g) t) +rename f g (Map m a b c) = Map m (renameBoundTy' f g a) (renameTy' f g b) (renameTy' f g c) +rename (Sugar f) g (QuasiQuote m t) = QuasiQuote m (rename (Quote g) f t) +rename (Quote f) g (Unquote m t) = Unquote m (rename (Sugar g) f t) +rename (Sugar f) g (QAbs m (bound ** t)) = + QAbs m (bound ** rename (Sugar (f <>< lengthOf bound)) g t) +rename (Sugar f) g (Lit m k) = Lit m k +rename (Sugar f) g (Suc m t) = Suc m (rename (Sugar f) g t) +rename (Sugar f) g (List m ts) = List m (renameList (Sugar f) g ts) +rename (Sugar f) g (Cons m t u) = Cons m (rename (Sugar f) g t) (rename (Sugar f) g u) +rename (Sugar f) g (Str m str) = Str m str +rename (Sugar f) g (FoldCase m e (MkRow ts fresh)) = + FoldCase m (rename (Sugar f) g e) (fromAll (renameBranches (Sugar f) g ts) fresh) + +renameList f g [] = [] +renameList f g (t :: ts) = rename f g t :: renameList f g ts + +renameAll f g [<] = [<] +renameAll f g (ts :< (x :- t)) = renameAll f g ts :< (x :- rename f g t) + +renameBranches f g [<] = [<] +renameBranches f g (ts :< (l :- (x ** t))) = + renameBranches f g ts :< (l :- (x ** rename f (Keep g) t)) + +renameTy' NoSugar g a = a +renameTy' (Sugar f) g a = a +renameTy' (Quote f) g t = rename (Sugar g) f t + +renameBoundTy' NoSugar g xa = xa +renameBoundTy' (Sugar f) g xa = xa +renameBoundTy' (Quote f) g t = rename (Sugar g) f t |