From 1ebeb5fd02ed86c2743e15c5b3ca2a489346db4d Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Fri, 7 Mar 2025 17:21:52 +0000 Subject: Rewrite for flap v2.0.0. Make `foldcase` syntactic sugar. --- src/Inky/Term/Desugar.idr | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Inky/Term/Desugar.idr') 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 |] -- cgit v1.2.3