Merge pull request #28 from fizruk/soas

SOAS package and better TH support for complex types

.gitignore

@@ -1,9 +1,15 @@
-haskell/free-foil/src/Language/LambdaPi/Syntax/Lex.hs
-haskell/free-foil/src/Language/LambdaPi/Syntax/Par.hs
-haskell/free-foil/src/Language/LambdaPi/Syntax/Test
-haskell/free-foil/src/Language/LambdaPi/Syntax/Test.hs
-haskell/free-foil/src/Language/LambdaPi/Syntax/Skel.hs
-haskell/free-foil/src/Language/LambdaPi/Syntax/ErrM.hs
+haskell/lambda-pi/src/Language/LambdaPi/Syntax/Lex.hs
+haskell/lambda-pi/src/Language/LambdaPi/Syntax/Par.hs
+haskell/lambda-pi/src/Language/LambdaPi/Syntax/Test
+haskell/lambda-pi/src/Language/LambdaPi/Syntax/Test.hs
+haskell/lambda-pi/src/Language/LambdaPi/Syntax/Skel.hs
+haskell/lambda-pi/src/Language/LambdaPi/Syntax/ErrM.hs
+haskell/soas/src/Language/SOAS/Syntax/Lex.hs
+haskell/soas/src/Language/SOAS/Syntax/Par.hs
+haskell/soas/src/Language/SOAS/Syntax/Test
+haskell/soas/src/Language/SOAS/Syntax/Test.hs
+haskell/soas/src/Language/SOAS/Syntax/Skel.hs
+haskell/soas/src/Language/SOAS/Syntax/ErrM.hs
 
 scala/free-foil/src/main/scala/.scala-build/
 

haskell/free-foil/free-foil.cabal

@@ -43,6 +43,7 @@ library
       Control.Monad.Free.Foil.Generic
       Control.Monad.Free.Foil.TH
       Control.Monad.Free.Foil.TH.Convert
+      Control.Monad.Free.Foil.TH.MkFreeFoil
       Control.Monad.Free.Foil.TH.PatternSynonyms
       Control.Monad.Free.Foil.TH.Signature
       Control.Monad.Free.Foil.TH.ZipMatch

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

@@ -47,7 +47,10 @@ module Control.Monad.Foil (
   Substitution,
   lookupSubst,
   identitySubst,
+  voidSubst,
   addSubst,
+  addSubstPattern,
+  addSubstList,
   addRename,
   -- * Unification of binders
   UnifyNameBinders(..),
@@ -66,6 +69,10 @@ module Control.Monad.Foil (
   emptyNameMap,
   lookupName,
   addNameBinder,
+  nameMapToSubstitution,
+  addNameBinders,
+  addNameBinderList,
+  NameBinderList(..),
   -- * Constraints
   Ext,
   ExtEvidence(..),

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

@@ -708,6 +708,35 @@ class CoSinkable (pattern :: S -> S -> Type) where
     -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
     -> r
 
+-- | Auxiliary data structure for collecting name binders. Used in 'nameBinderListOf'.
+newtype WithNameBinderList r n l (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)
+
+-- | Empty list of name binders (identity).
+idWithNameBinderList :: DExt o o' => WithNameBinderList r n n o o'
+idWithNameBinderList = WithNameBinderList id
+
+-- | Concatenating lists of name binders (compose).
+compWithNameBinderList
+  :: (DExt o o', DExt o' o'')
+  => WithNameBinderList r n i o o'
+  -> WithNameBinderList r i l o' o''
+  -> WithNameBinderList r n l o o''
+compWithNameBinderList (WithNameBinderList f) (WithNameBinderList g) =
+  WithNameBinderList (f . g)
+
+-- | Collect name binders of a generalized pattern into a name binder list,
+-- which can be more easily traversed.
+nameBinderListOf :: (CoSinkable binder) => binder n l -> NameBinderList n l
+nameBinderListOf pat = withPattern
+  (\_scope' binder k ->
+    unsafeAssertFresh binder $ \binder' ->
+      k (WithNameBinderList (NameBinderListCons binder)) binder')
+  idWithNameBinderList
+  compWithNameBinderList
+  emptyScope
+  pat
+  (\(WithNameBinderList f) _ -> f NameBinderListEmpty)
+
 instance CoSinkable NameBinder where
   coSinkabilityProof _rename (UnsafeNameBinder name) cont =
     cont unsafeCoerce (UnsafeNameBinder name)
@@ -733,6 +762,10 @@ identitySubst
   :: InjectName e => Substitution e i i
 identitySubst = UnsafeSubstitution IntMap.empty
 
+-- | An empty substitution from an empty scope.
+voidSubst :: Substitution e VoidS n
+voidSubst = UnsafeSubstitution IntMap.empty
+
 -- | Extend substitution with a particular mapping.
 addSubst
   :: Substitution e i o
@@ -742,6 +775,24 @@ addSubst
 addSubst (UnsafeSubstitution env) (UnsafeNameBinder (UnsafeName name)) ex
   = UnsafeSubstitution (IntMap.insert name ex env)
 
+addSubstPattern
+  :: CoSinkable binder
+  => Substitution e i o
+  -> binder i i'
+  -> [e o]
+  -> Substitution e i' o
+addSubstPattern subst pat = addSubstList subst (nameBinderListOf pat)
+
+addSubstList
+  :: Substitution e i o
+  -> NameBinderList i i'
+  -> [e o]
+  -> Substitution e i' o
+addSubstList subst NameBinderListEmpty _ = subst
+addSubstList subst (NameBinderListCons binder binders) (x:xs) =
+  addSubstList (addSubst subst binder x) binders xs
+addSubstList _ _ [] = error "cannot add a binder to Substitution since the value list does not have enough elements"
+
 -- | Add variable renaming to a substitution.
 -- This includes the performance optimization of eliding names mapped to themselves.
 addRename :: InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o
@@ -763,6 +814,29 @@ newtype NameMap (n :: S) a = NameMap { getNameMap :: IntMap a }
 emptyNameMap :: NameMap VoidS a
 emptyNameMap = NameMap IntMap.empty
 
+-- | Convert a 'NameMap' of expressions into a 'Substitution'.
+nameMapToSubstitution :: NameMap i (e o) -> Substitution e i o
+nameMapToSubstitution (NameMap m) = (UnsafeSubstitution m)
+
+-- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder').
+--
+-- Note that the input list is expected to have __at least__ the same number of elements
+-- as there are binders in the input pattern (generalized binder).
+addNameBinders :: CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a
+addNameBinders pat = addNameBinderList (nameBinderListOf pat)
+
+-- | Extend a map with multiple mappings (by repeatedly applying 'addNameBinder').
+--
+-- Note that the input list is expected to have __at least__ the same number of elements
+-- as there are binders in the input name binder list.
+--
+-- See also 'addNameBinders' for a generalized version.
+addNameBinderList :: NameBinderList n l -> [a] -> NameMap n a -> NameMap l a
+addNameBinderList NameBinderListEmpty _ = id
+addNameBinderList (NameBinderListCons binder binders) (x:xs) =
+  addNameBinderList binders xs . addNameBinder binder x
+addNameBinderList _ [] = error "cannot add a binder to NameMap since the value list does not have enough elements"
+
 -- | Looking up a name should always succeed.
 --
 -- Note that since 'Name' is 'Sinkable', you can lookup a name from scope @n@ in a 'NameMap' for scope @l@ whenever @l@ extends @n@.

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

@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds             #-}
-{-# LANGUAGE RankNTypes             #-}
 {-# LANGUAGE DeriveAnyClass        #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
@@ -9,6 +8,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes            #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE StandaloneDeriving    #-}
 {-# LANGUAGE UndecidableInstances  #-}
@@ -122,6 +122,20 @@ instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST
               subst' = extendSubst subst
            in ScopedAST binder' (Foil.rbind scope' body subst')
 
+-- | Substitution for a single generalized pattern.
+substitutePattern
+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder)
+  => Foil.Scope o                           -- ^ Resulting scope.
+  -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@.
+  -> binder' n i                            -- ^ Binders that extend scope @n@ to scope @i@.
+  -> [AST binder sig o]                     -- ^ A list of terms intended to serve as
+  -> AST binder sig i
+  -> AST binder sig o
+substitutePattern scope env binders args body =
+  substitute scope env' body
+  where
+    env' = Foil.addSubstPattern env binders args
+
 -- * \(\alpha\)-equivalence
 
 -- | Refresh (force) all binders in a term, minimizing the used indices.
@@ -338,7 +352,7 @@ convertFromAST
   -- ^ Peel back one layer of syntax.
   -> (rawIdent -> rawTerm)
   -- ^ Convert identifier into a raw variable term.
-  -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)
+  -> (forall x y. binder x y -> rawPattern)
   -- ^ Convert scope-safe pattern into a raw pattern.
   -> (rawTerm -> rawScopedTerm)
   -- ^ Wrap raw term into a scoped term.
@@ -362,7 +376,7 @@ convertFromScopedAST
   -- ^ Peel back one layer of syntax.
   -> (rawIdent -> rawTerm)
   -- ^ Convert identifier into a raw variable term.
-  -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)
+  -> (forall x y. binder x y -> rawPattern)
   -- ^ Convert scope-safe pattern into a raw pattern.
   -> (rawTerm -> rawScopedTerm)
   -- ^ Wrap raw term into a scoped term.
@@ -373,5 +387,5 @@ convertFromScopedAST
   -> (rawPattern, rawScopedTerm)
 convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case
   ScopedAST binder body ->
-    ( makePattern f binder
+    ( makePattern binder
     , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))

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

@@ -1,13 +1,13 @@
 {-# OPTIONS_GHC -Wno-missing-methods #-}
 {-# LANGUAGE AllowAmbiguousTypes      #-}
-{-# LANGUAGE MultiParamTypeClasses      #-}
-{-# LANGUAGE ConstraintKinds      #-}
-{-# LANGUAGE GADTs      #-}
-{-# LANGUAGE InstanceSigs      #-}
-{-# LANGUAGE DefaultSignatures      #-}
-{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE ConstraintKinds          #-}
 {-# LANGUAGE DataKinds                #-}
+{-# LANGUAGE DefaultSignatures        #-}
 {-# LANGUAGE FlexibleContexts         #-}
+{-# LANGUAGE FlexibleInstances        #-}
+{-# LANGUAGE GADTs                    #-}
+{-# LANGUAGE InstanceSigs             #-}
+{-# LANGUAGE MultiParamTypeClasses    #-}
 {-# LANGUAGE PolyKinds                #-}
 {-# LANGUAGE RankNTypes               #-}
 {-# LANGUAGE ScopedTypeVariables      #-}
@@ -18,7 +18,7 @@
 {-# LANGUAGE UndecidableInstances     #-}
 module Control.Monad.Free.Foil.Generic where
 
-import           Data.Kind     (Constraint, Type)
+import           Data.Kind              (Constraint, Type)
 import           Generics.Kind
 import           Generics.Kind.Examples ()
 import           GHC.TypeError