Derive withPattern via Template Haskell

fizruk · Jun 20, 2024 · 400f338 · 400f338
1 parent d694d6e
commit 400f338
Showing 1 changed file with 41 additions and 1 deletion.
diff --git a/haskell/free-foil/src/Control/Monad/Foil/TH/MkInstancesFoil.hs b/haskell/free-foil/src/Control/Monad/Foil/TH/MkInstancesFoil.hs
@@ -27,7 +27,8 @@ mkInstancesFoil termT nameT scopeT patternT = do
         [ FunD 'Foil.sinkabilityProof (map clauseScopedTerm scopeCons) ]
 
     , InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))
-        [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons) ]
+        [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons)
+        , FunD 'Foil.withPattern (map clauseWithPattern patternCons) ]
 
     , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilTermT (map (VarT . tvarName) termTVars)))
         [ FunD 'Foil.sinkabilityProof (map clauseTerm termCons)]
@@ -113,3 +114,42 @@ mkInstancesFoil termT nameT scopeT patternT = do
           go (i + 1) rename' (AppE p (VarE xi)) conPatterns
           where
             xi = mkName ("x" ++ show i)
+
+    clauseWithPattern :: Con -> Clause
+    clauseWithPattern RecC{} = error "Record constructors (RecC) are not supported yet!"
+    clauseWithPattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!"
+    clauseWithPattern ForallC{} = error "Existential constructors (ForallC) are not supported yet!"
+    clauseWithPattern GadtC{} = error "GADT constructors (GadtC) are not supported yet!"
+    clauseWithPattern RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"
+    clauseWithPattern (NormalC conName params) =
+      Clause
+        [VarP withNameBinder, VarP id', VarP comp, VarP scope, ConP foilConName [] conParamPatterns, VarP cont]
+        (NormalB (go 1 scope (VarE id') (ConE foilConName) params))
+        []
+      where
+        foilConName = mkName ("Foil" ++ nameBase conName)
+        withNameBinder = mkName "withNameBinder"
+        id' = mkName "id'"
+        comp = mkName "comp"
+        scope = mkName "scope"
+        cont = mkName "cont"
+        conParamPatterns = zipWith mkConParamPattern params [1..]
+        mkConParamPattern _ i = VarP (mkName ("x" ++ show i))
+
+        go _i _scope' rename' p [] = AppE (AppE (VarE cont) rename') p
+        go i scope' rename' p ((_bang, PeelConT tyName _tyParams) : conParams)
+          | tyName == nameT || tyName == patternT =
+              AppE
+                (foldl AppE (VarE 'Foil.withPattern) [VarE withNameBinder, VarE id', VarE comp, VarE scope', VarE xi])
+                (LamE [VarP renamei, VarP xi']
+                  (LetE [ValD (VarP scopei) (NormalB (AppE (AppE (VarE 'Foil.extendScopePattern) (VarE xi')) (VarE scope'))) []]
+                    (go (i + 1) scopei (foldl AppE (VarE comp) [rename', (VarE renamei)]) (AppE p (VarE xi')) conParams)))
+          where
+            xi = mkName ("x" ++ show i)
+            xi' = mkName ("x" ++ show i ++ "'")
+            renamei = mkName ("f" ++ show i)
+            scopei = mkName ("scope" ++ show i)
+        go i scope' rename' p (_ : conPatterns) =
+          go (i + 1) scope' rename' (AppE p (VarE xi)) conPatterns
+          where
+            xi = mkName ("x" ++ show i)