summaryrefslogtreecommitdiff
path: root/src/Inky/Term/Desugar.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2025-03-07 17:21:52 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2025-03-13 13:21:06 +0000
commit1ebeb5fd02ed86c2743e15c5b3ca2a489346db4d (patch)
treef88834cd7b029343a1ad4a5969258e4022fdd00d /src/Inky/Term/Desugar.idr
parentf5b75edd91389f0a45045b707abfa36c746e8d54 (diff)
Rewrite for flap v2.0.0.HEADmaster
Make `foldcase` syntactic sugar.
Diffstat (limited to 'src/Inky/Term/Desugar.idr')
-rw-r--r--src/Inky/Term/Desugar.idr12
1 files changed, 12 insertions, 0 deletions
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 |]