Add UnifiablePattern class and add pattern support in FreeFoilTH

haskell/free-foil/src/Control/Monad/Foil.hs

@@ -52,6 +52,8 @@ module Control.Monad.Foil (
   -- * Unification of binders
   UnifyNameBinders(..),
   unifyNameBinders,
+  andThenUnifyPatterns,
+  UnifiablePattern(..),
   -- ** Eliminating impossible unification
   V2, absurd2,
   -- * Name maps

haskell/free-foil/src/Control/Monad/Foil/Internal.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE BlockArguments             #-}
+{-# LANGUAGE LambdaCase             #-}
 {-# LANGUAGE EmptyCase             #-}
 {-# LANGUAGE ConstraintKinds            #-}
 {-# LANGUAGE DataKinds                  #-}
@@ -340,6 +341,8 @@ data UnifyNameBinders pattern n l r where
   RenameRightNameBinder :: (NameBinder n r -> NameBinder n l) -> UnifyNameBinders pattern n l r
   -- | It is necessary to rename both binders.
   RenameBothBinders :: pattern n lr -> (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> UnifyNameBinders pattern n l r
+  -- | Cannot unify to (sub)patterns.
+  NotUnifiable :: pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
 
 -- | Unify binders either by asserting that they are the same,
 -- or by providing a /safe/ renaming function to convert one binder to another.
@@ -355,6 +358,44 @@ unifyNameBinders (UnsafeNameBinder (UnsafeName i1)) (UnsafeNameBinder (UnsafeNam
   | otherwise = RenameLeftNameBinder $ \(UnsafeNameBinder (UnsafeName i')) ->
       if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i')
 
+unsafeMergeUnifyBinders :: UnifyNameBinders binder a a' a'' -> UnifyNameBinders binder b b' b'' -> UnifyNameBinders binder c c' c''
+unsafeMergeUnifyBinders = \case
+  SameNameBinders -> unsafeCoerce
+  u@(RenameLeftNameBinder f) -> \case
+    SameNameBinders -> unsafeCoerce u
+    RenameLeftNameBinder g -> RenameLeftNameBinder (unsafeCoerce f . unsafeCoerce g)
+    RenameRightNameBinder g -> RenameBothBinders undefined (unsafeCoerce f) (unsafeCoerce g)
+    RenameBothBinders _ f' g -> RenameBothBinders undefined (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)
+    NotUnifiable _ _ -> NotUnifiable undefined undefined
+  u@(RenameRightNameBinder f) -> \case
+    SameNameBinders -> unsafeCoerce u
+    RenameLeftNameBinder g -> RenameBothBinders undefined (unsafeCoerce f) (unsafeCoerce g)
+    RenameRightNameBinder g -> RenameRightNameBinder (unsafeCoerce f . unsafeCoerce g)
+    RenameBothBinders _ g f' -> RenameBothBinders undefined (unsafeCoerce g) (unsafeCoerce f . unsafeCoerce f')
+    NotUnifiable _ _ -> NotUnifiable undefined undefined
+  u@(RenameBothBinders _ f g) -> \case
+    SameNameBinders -> unsafeCoerce u
+    RenameLeftNameBinder f' -> RenameBothBinders undefined (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)
+    RenameRightNameBinder g' -> RenameBothBinders undefined (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')
+    RenameBothBinders _ f' g' -> RenameBothBinders undefined (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g . unsafeCoerce g')
+    NotUnifiable _ _ -> NotUnifiable undefined undefined
+  NotUnifiable _ _ -> const (NotUnifiable undefined undefined)
+
+andThenUnifyPatterns :: (UnifiablePattern binder) => UnifyNameBinders binder n l l' -> (binder l r, binder l' r') -> UnifyNameBinders binder n r r'
+andThenUnifyPatterns u = case u of
+  SameNameBinders -> uncurry (unsafeCoerce . unifyPatterns)
+  RenameLeftNameBinder renameL -> \(l, r) ->
+    extendNameBinderRenaming renameL l $ \_renameL' l' ->
+      unsafeMergeUnifyBinders u (unifyPatterns l' r)
+  RenameRightNameBinder renameR -> \(l, r) ->
+    extendNameBinderRenaming renameR r $ \_renameR' r' ->
+      unsafeMergeUnifyBinders u (unifyPatterns l r')
+  RenameBothBinders _ renameL renameR -> \(l, r) ->
+    extendNameBinderRenaming renameL l $ \_renameL' l' ->
+      extendNameBinderRenaming renameR r $ \_renameR' r' ->
+        unsafeMergeUnifyBinders u (unifyPatterns l' r')
+  NotUnifiable{} -> const (NotUnifiable undefined undefined)
+
 data V2 (n :: S) (l :: S)
 
 absurd2 :: V2 n l -> a

haskell/free-foil/src/Control/Monad/Free/Foil.hs

@@ -213,6 +213,8 @@ alphaEquivScoped scope
             in alphaEquiv scope'
                 (Foil.liftRM scope' (Foil.fromNameBinderRenaming rename1) body1)
                 (Foil.liftRM scope' (Foil.fromNameBinderRenaming rename2) body2)
+      -- if we cannot unify patterns then scopes are not alpha-equivalent
+      Foil.NotUnifiable _ _ -> False
 
 -- ** Unsafe equality checks
 

haskell/lambda-pi/app/LambdaPi.hs

@@ -1,6 +1,6 @@
 module Main where
 
-import qualified Language.LambdaPi.Impl.FreeFoil as FreeFoil
+import qualified Language.LambdaPi.Impl.FreeFoilTH as FreeFoilTH
 
 main :: IO ()
-main = FreeFoil.defaultMain
+main = FreeFoilTH.defaultMain

haskell/lambda-pi/src/Language/LambdaPi/Impl/Foil.hs

@@ -33,8 +33,7 @@
 -- 3. "Language.LambdaPi.Impl.FreeFoilTH" combines the benefits of the above, when it is possible to generate the signature automatically.
 module Language.LambdaPi.Impl.Foil where
 
-import           Control.Monad.Foil
-
+import           Control.Monad.Foil hiding (unifyPatterns)
 import           Control.Monad                   (join)
 import           Control.Monad.Foil.Relative
 import           Data.Coerce                     (coerce)
@@ -506,6 +505,7 @@ unifyPatterns (PatternVar x) (PatternVar x') cont =
       case (assertExt x, assertDistinct x) of
         (Ext, Distinct) -> Just (cont id renameR (PatternVar x))
     RenameBothBinders v2 _ _ -> absurd2 v2
+    NotUnifiable v2 _ -> absurd2 v2
 unifyPatterns (PatternPair l r) (PatternPair l' r') cont = join $
   unifyPatterns l l' $ \renameL renameL' l'' ->
     extendNameBinderRenaming renameL r $ \renameLext rext ->

haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs

@@ -1,11 +1,11 @@
 {-# LANGUAGE DataKinds         #-}
-{-# LANGUAGE RankNTypes         #-}
-{-# LANGUAGE GADTs             #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs             #-}
 {-# LANGUAGE KindSignatures    #-}
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE PatternSynonyms   #-}
+{-# LANGUAGE RankNTypes        #-}
 {-# LANGUAGE TemplateHaskell   #-}
 -- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
 --
@@ -32,8 +32,8 @@
 module Language.LambdaPi.Impl.FreeFoilTH where
 
 import qualified Control.Monad.Foil              as Foil
-import           Control.Monad.Free.Foil
 import           Control.Monad.Foil.TH
+import           Control.Monad.Free.Foil
 import           Control.Monad.Free.Foil.TH
 import           Data.Bifunctor.TH
 import           Data.Map                        (Map)
@@ -79,6 +79,13 @@ mkFromFoilPattern ''Raw.VarIdent ''Raw.Pattern'
 
 -- * User-defined code
 
+instance Foil.UnifiablePattern FoilPattern where
+  unifyPatterns (FoilPatternWildcard _loc) (FoilPatternWildcard _loc') = Foil.SameNameBinders
+  unifyPatterns (FoilPatternVar _loc x) (FoilPatternVar _loc' x') = Foil.unifyNameBinders x x'
+  unifyPatterns (FoilPatternPair _loc l r) (FoilPatternPair _loc' l' r') =
+    Foil.unifyPatterns l l' `Foil.andThenUnifyPatterns` (r, r')
+  unifyPatterns l r = Foil.NotUnifiable l r
+
 type Term' a = AST (FoilPattern' a) (Term'Sig a)
 type Term = Term' Raw.BNFC'Position
 type FoilPattern = FoilPattern' Raw.BNFC'Position
@@ -124,17 +131,19 @@ instance Show (AST (FoilPattern' a) (Term'Sig a) Foil.VoidS) where
 
 -- ** Evaluation
 
-matchPattern
-  :: Foil.Scope n
-  -> FoilPattern n l
-  -> Term n
-  -> Foil.Substitution Term l n
-matchPattern = undefined
+-- | Match a pattern against an term.
+matchPattern :: FoilPattern n l -> Term n -> Foil.Substitution Term l n
+matchPattern pat term = go pat term Foil.identitySubst
+  where
+    go :: FoilPattern i l -> Term n -> Foil.Substitution Term i n -> Foil.Substitution Term l n
+    go (FoilPatternWildcard _loc) _ = id
+    go (FoilPatternVar _loc x) e    = \subst -> Foil.addSubst subst x e
+    go (FoilPatternPair loc l r) e  = go r (Second loc e) . go l (First loc e)
 
 -- | Compute weak head normal form (WHNF) of a λΠ-term.
 --
--- >>> whnf Foil.emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)"
--- λ x0 . λ x1 . x1
+-- >>> whnf Foil.emptyScope "(λx.(λ_.x)(λy.x))(λ(y,z).z)"
+-- λ (x0, x1) . x1
 --
 -- >>> whnf Foil.emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))"
 -- λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1)
@@ -165,7 +174,7 @@ whnf scope = \case
   App loc f x ->
     case whnf scope f of
       Lam _loc binder body ->
-        let subst = matchPattern scope binder x
+        let subst = matchPattern binder x
          in whnf scope (substitute scope subst body)
       f' -> App loc f' x
   First loc t ->

haskell/lambda-pi/test/LambdaPi/test.in

@@ -12,6 +12,10 @@ check
   λ x. x
   : Π (x : A) → A
 
+compute
+  (λ (x, ( y , z)). y) ( ( (λ a . a) , (λ b. λ a. b, λ b. λ a. a)) )
+  : λ x. x
+
 compute
   (λ x. λ y. x) y
   : Π (w : A) → B